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  652  notbi  667  impidc  859  bijadc  883  pm2.13dc  886  xoranor  1396  mo2n  2081  necon3ad  2417  necon3bd  2418  nelcon3d  2481  ssneld  3194  sscon  3306  difrab  3446  exmid1stab  4251  eunex  4608  ndmfvg  5606  nnaord  6594  nnmord  6602  php5  6954  php5dom  6959  supmoti  7094  exmidomniim  7242  mkvprop  7259  enmkvlem  7262  prubl  7598  letr  8154  eqord1  8555  prodge0  8926  lt2msq  8958  nnge1  9058  nzadd  9424  irradd  9766  irrmul  9767  xrletr  9929  frec2uzf1od  10549  zesq  10801  expcanlem  10858  nn0opthd  10865  bccmpl  10897  fundm2domnop0  10988  maxleast  11466  fisumss  11645  dvdsbnd  12219  prm2orodd  12390  coprm  12408  prmndvdsfaclt  12420  hashgcdeq  12504  cos11  15267  bj-nnsn  15602  bj-nnelirr  15822  ismkvnnlem  15924  nconstwlpolem  15937