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  imandc  820  ianordc  833  pm5.17dc  844  dn1dc  902  xorbin  1316  xordc1  1325  alinexa  1535  dfrex2dc  2365  ralinexa  2399  rabeq0  3295  disj  3313  minel  3326  disjsn  3478  sotricim  4114  poirr2  4779  funun  5011  imadiflem  5046  imadif  5047  brprcneu  5246  prltlu  6949  caucvgprlemnbj  7129  caucvgprprlemnbj  7155  xrltnsym2  9159  fzp1nel  9411  phiprmpw  10978
  Copyright terms: Public domain W3C validator