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

Theorem con3i 562
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 558 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 544  ax-in2 545
This theorem is referenced by:  pm2.51  581  pm5.21ni  619  notnotnot  628  pm2.45  657  pm2.46  658  pm3.14  670  3ianorr  1204  nalequcoms  1410  equidqe  1425  ax6blem  1540  hbnt  1543  naecoms  1612  euor2  1958  moexexdc  1984  baroco  2007  necon3ai  2251  necon3bi  2252  eueq3dc  2712  difin  3171  indifdir  3190  difrab  3208  csbprc  3259  nelpri  3396  opprc  3567  opprc1  3568  opprc2  3569  eldifpw  4195  nlimsucg  4275  nfvres  5184  nfunsn  5185  ressnop0  5322  ovprc  5518  ovprc1  5519  ovprc2  5520  fiprc  6270  fidceq  6308  fzdcel  8862
  Copyright terms: Public domain W3C validator