Theorem con3d 636

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 634	. . 3 |- ( ch -> -. -. ch )
3	1, 2	syl6 33	. 2 |- ( ph -> ( ps -> -. -. ch ) )
4	3	con2d 629	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 619  ax-in2 620

This theorem is referenced by:  con3rr3  638  con3dimp  640  con3  647  nsyld  653  nsyli  654  jcn  657  notbi  672  impidc  866  bijadc  890  pm2.13dc  893  xoranor  1422  mo2n  2110  necon3ad  2456  necon3bd  2457  nelcon3d  2520  ssneld  3242  sscon  3355  difrab  3497  exmid1stab  4323  eunex  4685  ndmfvg  5703  suppssrst  6463  suppssrgst  6464  nnaord  6744  nnmord  6752  php5  7114  php5dom  7119  fidcen  7158  supmoti  7286  exmidomniim  7434  mkvprop  7451  enmkvlem  7454  prubl  7803  letr  8358  eqord1  8759  prodge0  9130  lt2msq  9162  nnge1  9262  nzadd  9632  irradd  9981  irrmul  9982  xrletr  10144  frec2uzf1od  10772  zesq  11024  expcanlem  11081  nn0opthd  11088  bccmpl  11120  fundm2domnop0  11224  maxleast  11902  fisumss  12082  dvdsbnd  12656  prm2orodd  12827  coprm  12845  prmndvdsfaclt  12857  hashgcdeq  12941  ballotfilemfc0  13153  ballotfilemfcc  13154  cos11  15735  bj-nnsn  16522  bj-nnelirr  16740  ismkvnnlem  16854  nconstwlpolem  16868