⊢ (f ⊃ g) ⊃ f ⊃ g | BaImpDist |
Proof:
1 | ⊢ (f ⊃ g) ⊃ ( f ⊃ g) | |
2 | ⊢ ( (f ⊃ g) ⊃ ( f ⊃ g)) | |
3 | ⊢ ( (f ⊃ g) ⊃ ( f ⊃ g)) ⊃ |
|
( (f ⊃ g) ⊃ ( f ⊃ g)) | ||
4 | ⊢ (f ⊃ g) ⊃ ( f ⊃ g) | |
5 | ⊢ (f ⊃ g) ≡ (f ⊃ g) | |
6 | ⊢ f ≡ f | |
7 | ⊢ g ≡ g | |
8 | ⊢ (f ⊃ g) ⊃ ( f ⊃ g) |
qed
Here are some easy corollaries:
⊢ | (f ≡ g) ⊃ f ≡ g | BaImpBaEqvBa |
⊢ | f ⊃ g ⇒ f ⊃ g | BaImpBa |
⊢ | f ≡ g ⇒ f ≡ g | BaEqvBa |
⊢ | f ⊃ g ⇒ f ⊃ g | DaImpDa |
⊢ | f ≡ g ⇒ f ≡ g | DaEqvDa |
⊢ | (f ∧ g) ≡ f ∧ g | BaAndEqv |
⊢ | (f1 ∧… ∧ fn) ≡ f1 ∧… ∧ fn | BaAndGroupEqv |