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  4292  eunex  4653  ndmfvg  5660  nnaord  6663  nnmord  6671  php5  7027  php5dom  7032  fidcen  7069  supmoti  7171  exmidomniim  7319  mkvprop  7336  enmkvlem  7339  prubl  7684  letr  8240  eqord1  8641  prodge0  9012  lt2msq  9044  nnge1  9144  nzadd  9510  irradd  9853  irrmul  9854  xrletr  10016  frec2uzf1od  10640  zesq  10892  expcanlem  10949  nn0opthd  10956  bccmpl  10988  fundm2domnop0  11080  maxleast  11739  fisumss  11918  dvdsbnd  12492  prm2orodd  12663  coprm  12681  prmndvdsfaclt  12693  hashgcdeq  12777  cos11  15542  bj-nnsn  16152  bj-nnelirr  16371  ismkvnnlem  16480  nconstwlpolem  16493