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  1388  mo2n  2070  necon3ad  2406  necon3bd  2407  nelcon3d  2470  ssneld  3181  sscon  3293  difrab  3433  exmid1stab  4237  eunex  4593  ndmfvg  5585  nnaord  6562  nnmord  6570  php5  6914  php5dom  6919  supmoti  7052  exmidomniim  7200  mkvprop  7217  enmkvlem  7220  prubl  7546  letr  8102  eqord1  8502  prodge0  8873  lt2msq  8905  nnge1  9005  nzadd  9369  irradd  9711  irrmul  9712  xrletr  9874  frec2uzf1od  10477  zesq  10729  expcanlem  10786  nn0opthd  10793  bccmpl  10825  maxleast  11357  fisumss  11535  dvdsbnd  12093  prm2orodd  12264  coprm  12282  prmndvdsfaclt  12294  hashgcdeq  12377  cos11  14988  bj-nnsn  15225  bj-nnelirr  15445  ismkvnnlem  15542  nconstwlpolem  15555