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  2108  necon3ad  2454  necon3bd  2455  nelcon3d  2518  ssneld  3240  sscon  3353  difrab  3495  exmid1stab  4321  eunex  4683  ndmfvg  5701  suppssrst  6461  suppssrgst  6462  nnaord  6742  nnmord  6750  php5  7112  php5dom  7117  fidcen  7156  supmoti  7284  exmidomniim  7432  mkvprop  7449  enmkvlem  7452  prubl  7801  letr  8356  eqord1  8757  prodge0  9128  lt2msq  9160  nnge1  9260  nzadd  9630  irradd  9978  irrmul  9979  xrletr  10141  frec2uzf1od  10768  zesq  11020  expcanlem  11077  nn0opthd  11084  bccmpl  11116  fundm2domnop0  11220  maxleast  11898  fisumss  12078  dvdsbnd  12652  prm2orodd  12823  coprm  12841  prmndvdsfaclt  12853  hashgcdeq  12937  cos11  15718  bj-nnsn  16505  bj-nnelirr  16723  ismkvnnlem  16837  nconstwlpolem  16851