ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  con3i Unicode 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  |-  ( ph  ->  ps )
Assertion
Ref Expression
con3i  |-  ( -. 
ps  ->  -.  ph )

Proof of Theorem con3i
StepHypRef Expression
1 id 19 . 2  |-  ( -. 
ps  ->  -.  ps )
2 con3i.a . 2  |-  ( ph  ->  ps )
31, 2nsyl 591 1  |-  ( -. 
ps  ->  -.  ph )
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  1241  nalequcoms  1451  equidqe  1466  ax6blem  1581  hbnt  1584  naecoms  1653  euor2  2000  moexexdc  2026  baroco  2049  necon3ai  2295  necon3bi  2296  eueq3dc  2767  difin  3208  indifdir  3227  difrab  3245  csbprc  3296  nelpri  3430  opprc  3599  opprc1  3600  opprc2  3601  eldifpw  4234  nlimsucg  4317  nfvres  5238  nfunsn  5239  ressnop0  5376  ovprc  5571  ovprc1  5572  ovprc2  5573  fiprc  6360  fidceq  6404  unfiexmid  6438  fzdcel  9135  bcpasc  9790  flodddiv4lt  10480
  Copyright terms: Public domain W3C validator