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  3159  sscon  3271  difrab  3411  exmid1stab  4210  eunex  4562  ndmfvg  5548  nnaord  6512  nnmord  6520  php5  6860  php5dom  6865  supmoti  6994  exmidomniim  7141  mkvprop  7158  enmkvlem  7161  prubl  7487  letr  8042  eqord1  8442  prodge0  8813  lt2msq  8845  nnge1  8944  nzadd  9307  irradd  9648  irrmul  9649  xrletr  9810  frec2uzf1od  10408  zesq  10641  expcanlem  10697  nn0opthd  10704  bccmpl  10736  maxleast  11224  fisumss  11402  dvdsbnd  11959  prm2orodd  12128  coprm  12146  prmndvdsfaclt  12158  hashgcdeq  12241  cos11  14313  bj-nnsn  14524  bj-nnelirr  14744  ismkvnnlem  14839  nconstwlpolem  14851