ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  pm4.55dc Structured version   GIF version

Theorem pm4.55dc 845
Description: Theorem *4.55 of [WhiteheadRussell] p. 120, for decidable propositions. (Contributed by Jim Kingdon, 2-May-2018.)
Assertion
Ref Expression
pm4.55dc (DECID φ → (DECID ψ → (¬ (¬ φ ψ) ↔ (φ ¬ ψ))))

Proof of Theorem pm4.55dc
StepHypRef Expression
1 pm4.54dc 804 . . . . 5 (DECID φ → (DECID ψ → ((¬ φ ψ) ↔ ¬ (φ ¬ ψ))))
21imp 115 . . . 4 ((DECID φ DECID ψ) → ((¬ φ ψ) ↔ ¬ (φ ¬ ψ)))
3 dcn 745 . . . . . . . . 9 (DECID ψDECID ¬ ψ)
43anim2i 324 . . . . . . . 8 ((DECID φ DECID ψ) → (DECID φ DECID ¬ ψ))
5 dcor 842 . . . . . . . . 9 (DECID φ → (DECID ¬ ψDECID (φ ¬ ψ)))
65imp 115 . . . . . . . 8 ((DECID φ DECID ¬ ψ) → DECID (φ ¬ ψ))
74, 6syl 14 . . . . . . 7 ((DECID φ DECID ψ) → DECID (φ ¬ ψ))
8 dcn 745 . . . . . . . . 9 (DECID φDECID ¬ φ)
9 dcan 841 . . . . . . . . 9 (DECID ¬ φ → (DECID ψDECIDφ ψ)))
108, 9syl 14 . . . . . . . 8 (DECID φ → (DECID ψDECIDφ ψ)))
1110imp 115 . . . . . . 7 ((DECID φ DECID ψ) → DECIDφ ψ))
127, 11jca 290 . . . . . 6 ((DECID φ DECID ψ) → (DECID (φ ¬ ψ) DECIDφ ψ)))
13 con2bidc 768 . . . . . . 7 (DECID (φ ¬ ψ) → (DECIDφ ψ) → (((φ ¬ ψ) ↔ ¬ (¬ φ ψ)) ↔ ((¬ φ ψ) ↔ ¬ (φ ¬ ψ)))))
1413imp 115 . . . . . 6 ((DECID (φ ¬ ψ) DECIDφ ψ)) → (((φ ¬ ψ) ↔ ¬ (¬ φ ψ)) ↔ ((¬ φ ψ) ↔ ¬ (φ ¬ ψ))))
1512, 14syl 14 . . . . 5 ((DECID φ DECID ψ) → (((φ ¬ ψ) ↔ ¬ (¬ φ ψ)) ↔ ((¬ φ ψ) ↔ ¬ (φ ¬ ψ))))
1615biimprd 147 . . . 4 ((DECID φ DECID ψ) → (((¬ φ ψ) ↔ ¬ (φ ¬ ψ)) → ((φ ¬ ψ) ↔ ¬ (¬ φ ψ))))
172, 16mpd 13 . . 3 ((DECID φ DECID ψ) → ((φ ¬ ψ) ↔ ¬ (¬ φ ψ)))
1817bicomd 129 . 2 ((DECID φ DECID ψ) → (¬ (¬ φ ψ) ↔ (φ ¬ ψ)))
1918ex 108 1 (DECID φ → (DECID ψ → (¬ (¬ φ ψ) ↔ (φ ¬ ψ))))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4   wa 97  wb 98   wo 628  DECID wdc 741
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 629
This theorem depends on definitions:  df-bi 110  df-dc 742
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator