Theorem con3d 626

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

This theorem is referenced by:  con3rr3  628  con3dimp  630  con3  637  nsyld  643  nsyli  644  jcn  646  notbi  661  impidc  853  bijadc  877  pm2.13dc  880  xoranor  1372  mo2n  2047  necon3ad  2382  necon3bd  2383  nelcon3d  2446  ssneld  3149  sscon  3261  difrab  3401  eunex  4545  ndmfvg  5527  nnaord  6488  nnmord  6496  php5  6836  php5dom  6841  supmoti  6970  exmidomniim  7117  mkvprop  7134  enmkvlem  7137  prubl  7448  letr  8002  eqord1  8402  prodge0  8770  lt2msq  8802  nnge1  8901  nzadd  9264  irradd  9605  irrmul  9606  xrletr  9765  frec2uzf1od  10362  zesq  10594  expcanlem  10649  nn0opthd  10656  bccmpl  10688  maxleast  11177  fisumss  11355  dvdsbnd  11911  prm2orodd  12080  coprm  12098  prmndvdsfaclt  12110  hashgcdeq  12193  cos11  13568  bj-nnsn  13768  bj-nnelirr  13988  exmid1stab  14033  ismkvnnlem  14084  nconstwlpolem  14096