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  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  nelprd  3457  opprc  3628  opprc1  3629  opprc2  3630  notnotsnex  3998  eldifpw  4274  nlimsucg  4357  nfvres  5302  nfunsn  5303  ressnop0  5443  ovprc  5643  ovprc1  5644  ovprc2  5645  mapprc  6363  fiprc  6486  fidceq  6539  unfiexmid  6582  fzdcel  9389  bcpasc  10092  flodddiv4lt  10861  nninfsellemsuc  11392
  Copyright terms: Public domain W3C validator