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

Theorem con3i 595
Description: A contraposition inference. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 20-Jun-2013.)
Hypothesis
Ref Expression
con3i.a (𝜑𝜓)
Assertion
Ref Expression
con3i 𝜓 → ¬ 𝜑)

Proof of Theorem con3i
StepHypRef Expression
1 id 19 . 2 𝜓 → ¬ 𝜓)
2 con3i.a . 2 (𝜑𝜓)
31, 2nsyl 591 1 𝜓 → ¬ 𝜑)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-in1 577  ax-in2 578
This theorem is referenced by:  pm2.51  614  pm5.21ni  652  notnotnot  661  pm2.45  690  pm2.46  691  pm3.14  703  3ianorr  1243  nalequcoms  1453  equidqe  1468  ax6blem  1583  hbnt  1586  naecoms  1656  euor2  2003  moexexdc  2029  baroco  2052  necon3ai  2300  necon3bi  2301  eueq3dc  2780  difin  3225  indifdir  3244  difrab  3262  csbprc  3316  ifandc  3413  nelpri  3455  opprc  3626  opprc1  3627  opprc2  3628  notnotsnex  3996  eldifpw  4272  nlimsucg  4355  nfvres  5300  nfunsn  5301  ressnop0  5441  ovprc  5641  ovprc1  5642  ovprc2  5643  mapprc  6361  fiprc  6484  fidceq  6537  unfiexmid  6580  fzdcel  9386  bcpasc  10070  flodddiv4lt  10811  nninfsellemsuc  11342
  Copyright terms: Public domain W3C validator