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

Theorem imnan 680
 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 627 . . . 4 (𝜑 → (𝜓 → ¬ (𝜑 → ¬ 𝜓)))
21imp 123 . . 3 ((𝜑𝜓) → ¬ (𝜑 → ¬ 𝜓))
32con2i 617 . 2 ((𝜑 → ¬ 𝜓) → ¬ (𝜑𝜓))
4 pm3.2 138 . . 3 (𝜑 → (𝜓 → (𝜑𝜓)))
54con3rr3 623 . 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 604  ax-in2 605 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  imnani  681  nan  682  pm3.24  683  imanst  874  ianordc  885  pm5.17dc  890  dn1dc  945  xorbin  1366  xordc1  1375  alinexa  1583  dfrex2dc  2448  ralinexa  2484  rabeq0  3423  disj  3442  minel  3455  disjsn  3621  sotricim  4282  poirr2  4975  funun  5211  imadiflem  5246  imadif  5247  brprcneu  5458  prltlu  7390  caucvgprlemnbj  7570  caucvgprprlemnbj  7596  suplocexprlemmu  7621  xrltnsym2  9683  fzp1nel  9988  fsumsplit  11286  sumsplitdc  11311  phiprmpw  12074  bj-nnor  13270
 Copyright terms: Public domain W3C validator