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  1396  mo2n  2081  necon3ad  2417  necon3bd  2418  nelcon3d  2481  ssneld  3194  sscon  3306  difrab  3446  exmid1stab  4251  eunex  4607  ndmfvg  5601  nnaord  6585  nnmord  6593  php5  6937  php5dom  6942  supmoti  7077  exmidomniim  7225  mkvprop  7242  enmkvlem  7245  prubl  7581  letr  8137  eqord1  8538  prodge0  8909  lt2msq  8941  nnge1  9041  nzadd  9407  irradd  9749  irrmul  9750  xrletr  9912  frec2uzf1od  10532  zesq  10784  expcanlem  10841  nn0opthd  10848  bccmpl  10880  maxleast  11443  fisumss  11622  dvdsbnd  12196  prm2orodd  12367  coprm  12385  prmndvdsfaclt  12397  hashgcdeq  12481  cos11  15243  bj-nnsn  15533  bj-nnelirr  15753  ismkvnnlem  15855  nconstwlpolem  15868