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

Theorem imnan 634
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 576 . . . 4 (𝜑 → (𝜓 → ¬ (𝜑 → ¬ 𝜓)))
21imp 119 . . 3 ((𝜑𝜓) → ¬ (𝜑 → ¬ 𝜓))
32con2i 567 . 2 ((𝜑 → ¬ 𝜓) → ¬ (𝜑𝜓))
4 pm3.2 130 . . 3 (𝜑 → (𝜓 → (𝜑𝜓)))
54con3rr3 573 . 2 (¬ (𝜑𝜓) → (𝜑 → ¬ 𝜓))
63, 5impbii 121 1 ((𝜑 → ¬ 𝜓) ↔ ¬ (𝜑𝜓))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 101  wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-in1 554  ax-in2 555
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  imnani  635  nan  636  pm3.24  637  imandc  797  ianordc  810  pm5.17dc  821  dn1dc  878  xorbin  1291  xordc1  1300  alinexa  1510  ralinexa  2368  pssn2lp  3072  rabeq0  3274  disj  3295  minel  3310  disjsn  3459  sotricim  4087  poirr2  4744  funun  4971  imadiflem  5005  imadif  5006  brprcneu  5198  prltlu  6642  caucvgprlemnbj  6822  caucvgprprlemnbj  6848  xrltnsym2  8815  fzp1nel  9067
  Copyright terms: Public domain W3C validator