Theorem con3d 640

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

Step	Hyp	Ref	Expression
1		con3d.1	. . 3 |- ( ph -> ( ps -> ch ) )
2		notnot 638	. . 3 |- ( ch -> -. -. ch )
3	1, 2	syl6 33	. 2 |- ( ph -> ( ps -> -. -. ch ) )
4	3	con2d 633	1 |- ( ph -> ( -. ch -> -. ps ) )

Syntax hints:   -. wn 3   -> wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in1 623  ax-in2 624

This theorem is referenced by:  con3rr3  642  con3dimp  644  con3  651  nsyld  657  nsyli  658  jcn  661  notbi  676  impidc  870  bijadc  894  pm2.13dc  897  xoranor  1426  mo2n  2114  necon3ad  2462  necon3bd  2463  nelcon3d  2526  ssneld  3250  sscon  3363  difrab  3507  exmid1stab  4340  eunex  4703  ndmfvg  5721  suppssrst  6491  suppssrgst  6492  nnaord  6772  nnmord  6780  php5  7149  php5dom  7154  fidcen  7193  supmoti  7323  exmidomniim  7471  mkvprop  7488  enmkvlem  7491  prubl  7843  letr  8398  eqord1  8801  prodge0  9174  lt2msq  9206  nnge1  9306  nzadd  9676  irradd  10025  irrmul  10026  xrletr  10189  frec2uzf1od  10821  zesq  11074  expcanlem  11131  nn0opthd  11138  bccmpl  11170  fundm2domnop0  11278  maxleast  11957  fisumss  12137  dvdsbnd  12711  prm2orodd  12882  coprm  12900  prmndvdsfaclt  12912  hashgcdeq  12996  ballotfilemfc0  13210  ballotfilemfcc  13211  cos11  15877  bj-nnsn  16675  bj-nnelirr  16893  ismkvnnlem  17007  nconstwlpolem  17020