Theorem con3d 631

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

This theorem is referenced by:  con3rr3  633  con3dimp  635  con3  642  nsyld  648  nsyli  649  jcn  651  notbi  666  impidc  858  bijadc  882  pm2.13dc  885  xoranor  1377  mo2n  2054  necon3ad  2389  necon3bd  2390  nelcon3d  2453  ssneld  3157  sscon  3269  difrab  3409  exmid1stab  4208  eunex  4560  ndmfvg  5546  nnaord  6509  nnmord  6517  php5  6857  php5dom  6862  supmoti  6991  exmidomniim  7138  mkvprop  7155  enmkvlem  7158  prubl  7484  letr  8038  eqord1  8438  prodge0  8809  lt2msq  8841  nnge1  8940  nzadd  9303  irradd  9644  irrmul  9645  xrletr  9806  frec2uzf1od  10403  zesq  10635  expcanlem  10690  nn0opthd  10697  bccmpl  10729  maxleast  11217  fisumss  11395  dvdsbnd  11951  prm2orodd  12120  coprm  12138  prmndvdsfaclt  12150  hashgcdeq  12233  cos11  14167  bj-nnsn  14367  bj-nnelirr  14587  ismkvnnlem  14682  nconstwlpolem  14694