Theorem con3d 634

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 632	. . 3 |- ( ch -> -. -. ch )
3	1, 2	syl6 33	. 2 |- ( ph -> ( ps -> -. -. ch ) )
4	3	con2d 627	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 617  ax-in2 618

This theorem is referenced by:  con3rr3  636  con3dimp  638  con3  645  nsyld  651  nsyli  652  jcn  655  notbi  670  impidc  863  bijadc  887  pm2.13dc  890  xoranor  1419  mo2n  2105  necon3ad  2442  necon3bd  2443  nelcon3d  2506  ssneld  3226  sscon  3338  difrab  3478  exmid1stab  4291  eunex  4652  ndmfvg  5657  nnaord  6653  nnmord  6661  php5  7015  php5dom  7020  supmoti  7156  exmidomniim  7304  mkvprop  7321  enmkvlem  7324  prubl  7669  letr  8225  eqord1  8626  prodge0  8997  lt2msq  9029  nnge1  9129  nzadd  9495  irradd  9837  irrmul  9838  xrletr  10000  frec2uzf1od  10623  zesq  10875  expcanlem  10932  nn0opthd  10939  bccmpl  10971  fundm2domnop0  11062  maxleast  11719  fisumss  11898  dvdsbnd  12472  prm2orodd  12643  coprm  12661  prmndvdsfaclt  12673  hashgcdeq  12757  cos11  15521  bj-nnsn  16055  bj-nnelirr  16274  ismkvnnlem  16379  nconstwlpolem  16392