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

Theorem imnan 690
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 637 . . . 4 (𝜑 → (𝜓 → ¬ (𝜑 → ¬ 𝜓)))
21imp 124 . . 3 ((𝜑𝜓) → ¬ (𝜑 → ¬ 𝜓))
32con2i 627 . 2 ((𝜑 → ¬ 𝜓) → ¬ (𝜑𝜓))
4 pm3.2 139 . . 3 (𝜑 → (𝜓 → (𝜑𝜓)))
54con3rr3 633 . 2 (¬ (𝜑𝜓) → (𝜑 → ¬ 𝜓))
63, 5impbii 126 1 ((𝜑 → ¬ 𝜓) ↔ ¬ (𝜑𝜓))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104  wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  imnani  691  nan  692  pm3.24  693  imanst  888  ianordc  899  pm5.17dc  904  dn1dc  960  xorbin  1384  xordc1  1393  alinexa  1603  dfrex2dc  2468  ralinexa  2504  rabeq0  3454  disj  3473  minel  3486  disjsn  3656  sotricim  4325  poirr2  5023  funun  5262  imadiflem  5297  imadif  5298  brprcneu  5510  2omotaplemap  7259  prltlu  7489  caucvgprlemnbj  7669  caucvgprprlemnbj  7695  suplocexprlemmu  7720  xrltnsym2  9797  fzp1nel  10107  fsumsplit  11418  sumsplitdc  11443  phiprmpw  12225  odzdvds  12248  pcdvdsb  12322  lgsne0  14600  bj-nnor  14647
  Copyright terms: Public domain W3C validator