Theorem con3d 603

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 601	. . 3 |- ( ch -> -. -. ch )
3	1, 2	syl6 33	. 2 |- ( ph -> ( ps -> -. -. ch ) )
4	3	con2d 596	1 |- ( ph -> ( -. ch -> -. ps ) )

Syntax hints:   -. wn 3   -> wi 4

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-in1 586  ax-in2 587

This theorem is referenced by:  con3rr3  605  con3dimp  607  con3  614  nsyld  620  nsyli  621  mth8  622  notbi  638  impidc  826  bijadc  850  pm2.13dc  853  xoranor  1338  mo2n  2003  necon3ad  2324  necon3bd  2325  nelcon3d  2388  ssneld  3065  sscon  3176  difrab  3316  eunex  4436  ndmfvg  5406  nnaord  6359  nnmord  6367  php5  6705  php5dom  6710  supmoti  6832  exmidomniim  6963  mkvprop  6982  prubl  7242  letr  7770  eqord1  8164  cnstab  8324  prodge0  8522  lt2msq  8554  nnge1  8653  nzadd  9010  irradd  9340  irrmul  9341  xrletr  9484  frec2uzf1od  10072  zesq  10303  expcanlem  10355  nn0opthd  10361  bccmpl  10393  maxleast  10877  fisumss  11053  efler  11256  dvdsbnd  11493  prm2orodd  11653  coprm  11668  prmndvdsfaclt  11680  hashgcdeq  11749  bj-nnsn  12638  bj-nnelirr  12843  exmid1stab  12887