Th35.) (I ⇒ J), (J ⇒ I) ⊢ (I ⇔ J)
1.) ⊢ I ⇒ J Hyp
2.) ⊢ J ⇒ I Hyp
3.) ⊢ (I ⇒ J) ⇒ [(J ⇒ I) ⇒ ((I ⇒ J) ∧ (J ⇒ I))] Th30
4.) ⊢ (J ⇒ I) ⇒ ((I ⇒ J) ∧ (J ⇒ I)) MP 1,3
5.) ⊢ (I ⇒ J) ∧ (J ⇒ I) MP 2,4
6.) ⊢ (I ⇔ J) Definition of ⇔
Th36.) H ⇔ K ⊢ K ⇔ H Symmetry of ⇔
1.) ⊢ H ⇔ K Hyp
2.) ⊢ (H ⇒ K) ∧ (K ⇒ H) Definition of ⇔
3.) ⊢ [(H ⇒ K) ∧ (K ⇒ H)] ⇒ [(K ⇒ H) ∧ (H ⇒ K)] Th27
4.) ⊢ (K ⇒ H) ∧ (H ⇒ K) MP 2,3
5.) ⊢ K ⇔ H Definition of ⇔
Th37.) (H ⇔ K), (K ⇔ L) ⊢ (H ⇔ L) Transitivity of ⇔
1.) H ⇔ K Hyp
2.) K ⇔ L Hyp
3.) ⊢ (H ⇒ K) ∧ (K ⇒ H) Definition of ⇔
4.) ⊢ (K ⇒ L) ∧ (L ⇒ K) Definition of ⇔
5.) ⊢ [(H ⇒ K) ∧ (K ⇒ H)] ⇒ (K ⇒ H) Th28
6.) ⊢ [(H ⇒ K) ∧ (K ⇒ H)] ⇒ (H ⇒ K) Th29
7.) ⊢ (K ⇒ H) MP 3,5
8.) ⊢ (H ⇒ K) MP 3,6
9.) ⊢ [(K ⇒ L) ∧ (L ⇒ K)] ⇒ (L ⇒ K) Th28
10.) ⊢ [(K ⇒ L) ∧ (L ⇒ K)] ⇒ (K ⇒ L) Th29
11.) ⊢ (L ⇒ K) MP 4,9
12.) ⊢ (K ⇒ L) MP 4,10
13.) ⊢ (H ⇒ L) Th5
14.) ⊢ (L ⇒ H) Th5
18.) ⊢ H ⇔ L Th35
No comments:
Post a Comment