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

Theorem dn1dc 853
 Description: DN1 for decidable propositions. Without the decidability conditions, DN1 can serve as a single axiom for Boolean algebra. See http://www-unix.mcs.anl.gov/~mccune/papers/basax/v12.pdf. (Contributed by Jim Kingdon, 22-Apr-2018.)
Assertion
Ref Expression
dn1dc ((DECID φ (DECID ψ (DECID χ DECID θ))) → (¬ (¬ (¬ (φ ψ) χ) ¬ (φ ¬ (¬ χ ¬ (χ θ)))) ↔ χ))

Proof of Theorem dn1dc
StepHypRef Expression
1 pm2.45 644 . . . . 5 (¬ (φ ψ) → ¬ φ)
2 imnan 611 . . . . 5 ((¬ (φ ψ) → ¬ φ) ↔ ¬ (¬ (φ ψ) φ))
31, 2mpbi 133 . . . 4 ¬ (¬ (φ ψ) φ)
43biorfi 652 . . 3 (χ ↔ (χ (¬ (φ ψ) φ)))
5 orcom 634 . . 3 ((χ (¬ (φ ψ) φ)) ↔ ((¬ (φ ψ) φ) χ))
6 ordir 718 . . 3 (((¬ (φ ψ) φ) χ) ↔ ((¬ (φ ψ) χ) (φ χ)))
74, 5, 63bitri 195 . 2 (χ ↔ ((¬ (φ ψ) χ) (φ χ)))
8 pm4.45 685 . . . . . 6 (χ ↔ (χ (χ θ)))
9 simprrl 479 . . . . . . 7 ((DECID φ (DECID ψ (DECID χ DECID θ))) → DECID χ)
10 dcor 829 . . . . . . . . 9 (DECID χ → (DECID θDECID (χ θ)))
1110imp 115 . . . . . . . 8 ((DECID χ DECID θ) → DECID (χ θ))
1211ad2antll 464 . . . . . . 7 ((DECID φ (DECID ψ (DECID χ DECID θ))) → DECID (χ θ))
13 anordc 849 . . . . . . 7 (DECID χ → (DECID (χ θ) → ((χ (χ θ)) ↔ ¬ (¬ χ ¬ (χ θ)))))
149, 12, 13sylc 56 . . . . . 6 ((DECID φ (DECID ψ (DECID χ DECID θ))) → ((χ (χ θ)) ↔ ¬ (¬ χ ¬ (χ θ))))
158, 14syl5bb 181 . . . . 5 ((DECID φ (DECID ψ (DECID χ DECID θ))) → (χ ↔ ¬ (¬ χ ¬ (χ θ))))
1615orbi2d 691 . . . 4 ((DECID φ (DECID ψ (DECID χ DECID θ))) → ((φ χ) ↔ (φ ¬ (¬ χ ¬ (χ θ)))))
1716anbi2d 440 . . 3 ((DECID φ (DECID ψ (DECID χ DECID θ))) → (((¬ (φ ψ) χ) (φ χ)) ↔ ((¬ (φ ψ) χ) (φ ¬ (¬ χ ¬ (χ θ))))))
18 dcor 829 . . . . . . . 8 (DECID φ → (DECID ψDECID (φ ψ)))
19 dcn 734 . . . . . . . 8 (DECID (φ ψ) → DECID ¬ (φ ψ))
2018, 19syl6 29 . . . . . . 7 (DECID φ → (DECID ψDECID ¬ (φ ψ)))
2120imp 115 . . . . . 6 ((DECID φ DECID ψ) → DECID ¬ (φ ψ))
2221adantrr 451 . . . . 5 ((DECID φ (DECID ψ (DECID χ DECID θ))) → DECID ¬ (φ ψ))
23 dcor 829 . . . . 5 (DECID ¬ (φ ψ) → (DECID χDECID (¬ (φ ψ) χ)))
2422, 9, 23sylc 56 . . . 4 ((DECID φ (DECID ψ (DECID χ DECID θ))) → DECID (¬ (φ ψ) χ))
25 dcn 734 . . . . . . . 8 (DECID χDECID ¬ χ)
269, 25syl 14 . . . . . . 7 ((DECID φ (DECID ψ (DECID χ DECID θ))) → DECID ¬ χ)
27 dcn 734 . . . . . . . 8 (DECID (χ θ) → DECID ¬ (χ θ))
2812, 27syl 14 . . . . . . 7 ((DECID φ (DECID ψ (DECID χ DECID θ))) → DECID ¬ (χ θ))
29 dcor 829 . . . . . . 7 (DECID ¬ χ → (DECID ¬ (χ θ) → DECIDχ ¬ (χ θ))))
3026, 28, 29sylc 56 . . . . . 6 ((DECID φ (DECID ψ (DECID χ DECID θ))) → DECIDχ ¬ (χ θ)))
31 dcn 734 . . . . . 6 (DECIDχ ¬ (χ θ)) → DECID ¬ (¬ χ ¬ (χ θ)))
3230, 31syl 14 . . . . 5 ((DECID φ (DECID ψ (DECID χ DECID θ))) → DECID ¬ (¬ χ ¬ (χ θ)))
33 dcor 829 . . . . . 6 (DECID φ → (DECID ¬ (¬ χ ¬ (χ θ)) → DECID (φ ¬ (¬ χ ¬ (χ θ)))))
3433imp 115 . . . . 5 ((DECID φ DECID ¬ (¬ χ ¬ (χ θ))) → DECID (φ ¬ (¬ χ ¬ (χ θ))))
3532, 34syldan 266 . . . 4 ((DECID φ (DECID ψ (DECID χ DECID θ))) → DECID (φ ¬ (¬ χ ¬ (χ θ))))
36 anordc 849 . . . 4 (DECID (¬ (φ ψ) χ) → (DECID (φ ¬ (¬ χ ¬ (χ θ))) → (((¬ (φ ψ) χ) (φ ¬ (¬ χ ¬ (χ θ)))) ↔ ¬ (¬ (¬ (φ ψ) χ) ¬ (φ ¬ (¬ χ ¬ (χ θ)))))))
3724, 35, 36sylc 56 . . 3 ((DECID φ (DECID ψ (DECID χ DECID θ))) → (((¬ (φ ψ) χ) (φ ¬ (¬ χ ¬ (χ θ)))) ↔ ¬ (¬ (¬ (φ ψ) χ) ¬ (φ ¬ (¬ χ ¬ (χ θ))))))
3817, 37bitrd 177 . 2 ((DECID φ (DECID ψ (DECID χ DECID θ))) → (((¬ (φ ψ) χ) (φ χ)) ↔ ¬ (¬ (¬ (φ ψ) χ) ¬ (φ ¬ (¬ χ ¬ (χ θ))))))
397, 38syl5rbb 182 1 ((DECID φ (DECID ψ (DECID χ DECID θ))) → (¬ (¬ (¬ (φ ψ) χ) ¬ (φ ¬ (¬ χ ¬ (χ θ)))) ↔ χ))
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 97   ↔ wb 98   ∨ wo 616  DECID wdc 730 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 532  ax-in2 533  ax-io 617 This theorem depends on definitions:  df-bi 110  df-dc 731 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator