| ⊢ (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 |