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

Theorem imnan 664
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 611 . . . 4 (𝜑 → (𝜓 → ¬ (𝜑 → ¬ 𝜓)))
21imp 123 . . 3 ((𝜑𝜓) → ¬ (𝜑 → ¬ 𝜓))
32con2i 601 . 2 ((𝜑 → ¬ 𝜓) → ¬ (𝜑𝜓))
4 pm3.2 138 . . 3 (𝜑 → (𝜓 → (𝜑𝜓)))
54con3rr3 607 . 2 (¬ (𝜑𝜓) → (𝜑 → ¬ 𝜓))
63, 5impbii 125 1 ((𝜑 → ¬ 𝜓) ↔ ¬ (𝜑𝜓))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 103  wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 588  ax-in2 589
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  imnani  665  nan  666  pm3.24  667  imanst  858  ianordc  869  pm5.17dc  874  dn1dc  929  xorbin  1347  xordc1  1356  alinexa  1567  dfrex2dc  2405  ralinexa  2439  rabeq0  3362  disj  3381  minel  3394  disjsn  3555  sotricim  4215  poirr2  4901  funun  5137  imadiflem  5172  imadif  5173  brprcneu  5382  prltlu  7263  caucvgprlemnbj  7443  caucvgprprlemnbj  7469  suplocexprlemmu  7494  xrltnsym2  9548  fzp1nel  9852  fsumsplit  11144  sumsplitdc  11169  phiprmpw  11825  bj-nnor  12873
  Copyright terms: Public domain W3C validator