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

Theorem imnan 624
 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 566 . . . 4 (𝜑 → (𝜓 → ¬ (𝜑 → ¬ 𝜓)))
21imp 115 . . 3 ((𝜑𝜓) → ¬ (𝜑 → ¬ 𝜓))
32con2i 557 . 2 ((𝜑 → ¬ 𝜓) → ¬ (𝜑𝜓))
4 pm3.2 126 . . 3 (𝜑 → (𝜓 → (𝜑𝜓)))
54con3rr3 563 . 2 (¬ (𝜑𝜓) → (𝜑 → ¬ 𝜓))
63, 5impbii 117 1 ((𝜑 → ¬ 𝜓) ↔ ¬ (𝜑𝜓))
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 97   ↔ wb 98 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545 This theorem depends on definitions:  df-bi 110 This theorem is referenced by:  imnani  625  nan  626  pm3.24  627  imandc  786  ianordc  799  pm5.17dc  810  dn1dc  867  xorbin  1275  xordc1  1284  alinexa  1494  ralinexa  2351  pssn2lp  3045  rabeq0  3247  disj  3268  minel  3283  disjsn  3432  sotricim  4060  poirr2  4717  funun  4944  imadiflem  4978  imadif  4979  brprcneu  5171  prltlu  6585  caucvgprlemnbj  6765  caucvgprprlemnbj  6791  xrltnsym2  8715  fzp1nel  8966
 Copyright terms: Public domain W3C validator