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  3182  sscon  3294  difrab  3434  exmid1stab  4238  eunex  4594  ndmfvg  5586  nnaord  6564  nnmord  6572  php5  6916  php5dom  6921  supmoti  7054  exmidomniim  7202  mkvprop  7219  enmkvlem  7222  prubl  7548  letr  8104  eqord1  8504  prodge0  8875  lt2msq  8907  nnge1  9007  nzadd  9372  irradd  9714  irrmul  9715  xrletr  9877  frec2uzf1od  10480  zesq  10732  expcanlem  10789  nn0opthd  10796  bccmpl  10828  maxleast  11360  fisumss  11538  dvdsbnd  12096  prm2orodd  12267  coprm  12285  prmndvdsfaclt  12297  hashgcdeq  12380  cos11  15029  bj-nnsn  15295  bj-nnelirr  15515  ismkvnnlem  15612  nconstwlpolem  15625