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

Theorem pclem6 1250
 Description: Negation inferred from embedded conjunct. (Contributed by NM, 20-Aug-1993.) (Proof rewritten by Jim Kingdon, 4-May-2018.)
Assertion
Ref Expression
pclem6 ((φ ↔ (ψ ¬ φ)) → ¬ ψ)

Proof of Theorem pclem6
StepHypRef Expression
1 bi1 111 . . . . 5 ((φ ↔ (ψ ¬ φ)) → (φ → (ψ ¬ φ)))
2 pm3.4 316 . . . . . 6 ((ψ ¬ φ) → (ψ → ¬ φ))
32com12 27 . . . . 5 (ψ → ((ψ ¬ φ) → ¬ φ))
41, 3syl9r 67 . . . 4 (ψ → ((φ ↔ (ψ ¬ φ)) → (φ → ¬ φ)))
5 ax-ia3 101 . . . . 5 (ψ → (¬ φ → (ψ ¬ φ)))
6 bi2 121 . . . . 5 ((φ ↔ (ψ ¬ φ)) → ((ψ ¬ φ) → φ))
75, 6syl9 66 . . . 4 (ψ → ((φ ↔ (ψ ¬ φ)) → (¬ φφ)))
84, 7impbidd 118 . . 3 (ψ → ((φ ↔ (ψ ¬ φ)) → (φ ↔ ¬ φ)))
9 pm5.19 609 . . . 4 ¬ (φ ↔ ¬ φ)
109pm2.21i 562 . . 3 ((φ ↔ ¬ φ) → ⊥ )
118, 10syl6com 31 . 2 ((φ ↔ (ψ ¬ φ)) → (ψ → ⊥ ))
12 dfnot 1247 . 2 ψ ↔ (ψ → ⊥ ))
1311, 12sylibr 137 1 ((φ ↔ (ψ ¬ φ)) → ¬ ψ)
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 97   ↔ wb 98   ⊥ wfal 1233 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 This theorem depends on definitions:  df-bi 110  df-tru 1231  df-fal 1234 This theorem is referenced by:  nalset  3861  pwnss  3886  bj-nalset  7118
 Copyright terms: Public domain W3C validator