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

Theorem imnan 623
 Description: Express implication in terms of conjunction. (Contributed by NM, 9-Apr-1994.) (Revised by Mario Carneiro, 1-Feb-2015.)
Assertion
Ref Expression
imnan ((φ → ¬ ψ) ↔ ¬ (φ ψ))

Proof of Theorem imnan
StepHypRef Expression
1 pm3.2im 565 . . . 4 (φ → (ψ → ¬ (φ → ¬ ψ)))
21imp 115 . . 3 ((φ ψ) → ¬ (φ → ¬ ψ))
32con2i 557 . 2 ((φ → ¬ ψ) → ¬ (φ ψ))
4 pm3.2 126 . . 3 (φ → (ψ → (φ ψ)))
54con3rr3 562 . 2 (¬ (φ ψ) → (φ → ¬ ψ))
63, 5impbii 117 1 ((φ → ¬ ψ) ↔ ¬ (φ ψ))
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 97   ↔ wb 98 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 This theorem depends on definitions:  df-bi 110 This theorem is referenced by:  imnani  624  nan  625  pm3.24  626  imandc  785  ianordc  798  pm5.17dc  809  dn1dc  866  xorbin  1272  xordc1  1281  mpto1  1311  alinexa  1491  ralinexa  2345  pssn2lp  3039  rabeq0  3241  disj  3262  minel  3277  disjsn  3423  sotricim  4051  poirr2  4660  funun  4887  imadiflem  4921  imadif  4922  brprcneu  5114  prltlu  6470  caucvgprlemnbj  6638  xrltnsym2  8485  fzp1nel  8736
 Copyright terms: Public domain W3C validator