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  865  bijadc  889  pm2.13dc  892  xoranor  1421  mo2n  2107  necon3ad  2444  necon3bd  2445  nelcon3d  2508  ssneld  3229  sscon  3341  difrab  3481  exmid1stab  4298  eunex  4659  ndmfvg  5670  nnaord  6677  nnmord  6685  php5  7044  php5dom  7049  fidcen  7088  supmoti  7192  exmidomniim  7340  mkvprop  7357  enmkvlem  7360  prubl  7706  letr  8262  eqord1  8663  prodge0  9034  lt2msq  9066  nnge1  9166  nzadd  9532  irradd  9880  irrmul  9881  xrletr  10043  frec2uzf1od  10669  zesq  10921  expcanlem  10978  nn0opthd  10985  bccmpl  11017  fundm2domnop0  11113  maxleast  11791  fisumss  11971  dvdsbnd  12545  prm2orodd  12716  coprm  12734  prmndvdsfaclt  12746  hashgcdeq  12830  cos11  15596  bj-nnsn  16380  bj-nnelirr  16599  ismkvnnlem  16708  nconstwlpolem  16721