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

Theorem con3d 561
Description: A contraposition deduction. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 31-Jan-2015.)
Hypothesis
Ref Expression
con3d.1  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
con3d  |-  ( ph  ->  ( -.  ch  ->  -. 
ps ) )

Proof of Theorem con3d
StepHypRef Expression
1 con3d.1 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
2 notnot 559 . . 3  |-  ( ch 
->  -.  -.  ch )
31, 2syl6 29 . 2  |-  ( ph  ->  ( ps  ->  -.  -.  ch ) )
43con2d 554 1  |-  ( ph  ->  ( -.  ch  ->  -. 
ps ) )
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:  con3rr3  563  con3and  564  con3  571  nsyld  577  nsyli  578  mth8  579  notbid  592  impidc  755  bijadc  776  pm2.13dc  779  xoranor  1268  mo2n  1928  necon3ad  2247  necon3bd  2248  ssneld  2947  sscon  3077  difrab  3211  eunex  4285  ndmfvg  5204  nnaord  6082  nnmord  6090  php5  6321  php5dom  6325  prubl  6582  letr  7099  prodge0  7818  lt2msq  7850  nnge1  7935  irradd  8578  irrmul  8579  xrletr  8722  frec2uzf1od  9166  zesq  9341  bj-notbi  10018  bj-nnelirr  10051
  Copyright terms: Public domain W3C validator