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

Theorem con3i 604
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 600 1  |-  ( -. 
ps  ->  -.  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in1 586  ax-in2 587
This theorem is referenced by:  notnotnot  606  conax1  625  pm5.21ni  675  pm2.45  710  pm2.46  711  pm3.14  725  3ianorr  1270  nalequcoms  1480  equidqe  1495  ax6blem  1611  hbnt  1614  naecoms  1685  euor2  2033  moexexdc  2059  baroco  2082  necon3ai  2332  necon3bi  2333  eueq3dc  2829  difin  3281  indifdir  3300  difrab  3318  csbprc  3376  ifandc  3476  nelpri  3519  nelprd  3521  opprc  3694  opprc1  3695  opprc2  3696  notnotsnex  4079  eldifpw  4366  nlimsucg  4449  nfvres  5420  nfunsn  5421  ressnop0  5567  ovprc  5772  ovprc1  5773  ovprc2  5774  mapprc  6512  ixpprc  6579  ixp0  6591  fiprc  6675  fidceq  6729  unfiexmid  6772  difinfsnlem  6950  fzdcel  9760  bcpasc  10452  flodddiv4lt  11529  bj-nnan  12759  bj-nnal  12760  bj-nnst  12775  nninfsellemsuc  13019
  Copyright terms: Public domain W3C validator