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

Theorem con3d 571
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 569 . . 3  |-  ( ch 
->  -.  -.  ch )
31, 2syl6 33 . 2  |-  ( ph  ->  ( ps  ->  -.  -.  ch ) )
43con2d 564 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 554  ax-in2 555
This theorem is referenced by:  con3rr3  573  con3dimp  574  con3  581  nsyld  587  nsyli  588  mth8  589  notbid  602  impidc  766  bijadc  787  pm2.13dc  790  xoranor  1284  mo2n  1944  necon3ad  2262  necon3bd  2263  ssneld  2975  sscon  3105  difrab  3239  eunex  4313  ndmfvg  5232  nnaord  6113  nnmord  6121  php5  6352  php5dom  6356  supmoti  6399  prubl  6642  letr  7160  prodge0  7895  lt2msq  7927  nnge1  8013  nzadd  8354  irradd  8678  irrmul  8679  xrletr  8825  frec2uzf1od  9356  zesq  9535  nn0opthd  9590  bccmpl  9622  bj-notbi  10432  bj-nnelirr  10465
  Copyright terms: Public domain W3C validator