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

Theorem imnan 657
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 599 . . . 4 (𝜑 → (𝜓 → ¬ (𝜑 → ¬ 𝜓)))
21imp 122 . . 3 ((𝜑𝜓) → ¬ (𝜑 → ¬ 𝜓))
32con2i 590 . 2 ((𝜑 → ¬ 𝜓) → ¬ (𝜑𝜓))
4 pm3.2 137 . . 3 (𝜑 → (𝜓 → (𝜑𝜓)))
54con3rr3 596 . 2 (¬ (𝜑𝜓) → (𝜑 → ¬ 𝜓))
63, 5impbii 124 1 ((𝜑 → ¬ 𝜓) ↔ ¬ (𝜑𝜓))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 102  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  imnani  658  nan  659  pm3.24  660  imanst  777  imandc  822  ianordc  835  pm5.17dc  846  dn1dc  904  xorbin  1318  xordc1  1327  alinexa  1537  dfrex2dc  2367  ralinexa  2401  rabeq0  3301  disj  3319  minel  3332  disjsn  3487  sotricim  4124  poirr2  4791  funun  5023  imadiflem  5058  imadif  5059  brprcneu  5261  prltlu  6990  caucvgprlemnbj  7170  caucvgprprlemnbj  7196  xrltnsym2  9196  fzp1nel  9448  phiprmpw  11073
  Copyright terms: Public domain W3C validator