Theorem con3d 632

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 630	. . 3 |- ( ch -> -. -. ch )
3	1, 2	syl6 33	. 2 |- ( ph -> ( ps -> -. -. ch ) )
4	3	con2d 625	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 615  ax-in2 616

This theorem is referenced by:  con3rr3  634  con3dimp  636  con3  643  nsyld  649  nsyli  650  jcn  653  notbi  668  impidc  860  bijadc  884  pm2.13dc  887  xoranor  1397  mo2n  2083  necon3ad  2419  necon3bd  2420  nelcon3d  2483  ssneld  3199  sscon  3311  difrab  3451  exmid1stab  4260  eunex  4617  ndmfvg  5620  nnaord  6608  nnmord  6616  php5  6970  php5dom  6975  supmoti  7110  exmidomniim  7258  mkvprop  7275  enmkvlem  7278  prubl  7619  letr  8175  eqord1  8576  prodge0  8947  lt2msq  8979  nnge1  9079  nzadd  9445  irradd  9787  irrmul  9788  xrletr  9950  frec2uzf1od  10573  zesq  10825  expcanlem  10882  nn0opthd  10889  bccmpl  10921  fundm2domnop0  11012  maxleast  11599  fisumss  11778  dvdsbnd  12352  prm2orodd  12523  coprm  12541  prmndvdsfaclt  12553  hashgcdeq  12637  cos11  15400  bj-nnsn  15808  bj-nnelirr  16027  ismkvnnlem  16132  nconstwlpolem  16145