Theorem con3d 636

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 634	. . 3 |- ( ch -> -. -. ch )
3	1, 2	syl6 33	. 2 |- ( ph -> ( ps -> -. -. ch ) )
4	3	con2d 629	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 619  ax-in2 620

This theorem is referenced by:  con3rr3  638  con3dimp  640  con3  647  nsyld  653  nsyli  654  jcn  657  notbi  672  impidc  865  bijadc  889  pm2.13dc  892  xoranor  1421  mo2n  2107  necon3ad  2444  necon3bd  2445  nelcon3d  2508  ssneld  3229  sscon  3341  difrab  3481  exmid1stab  4298  eunex  4659  ndmfvg  5670  nnaord  6676  nnmord  6684  php5  7043  php5dom  7048  fidcen  7087  supmoti  7191  exmidomniim  7339  mkvprop  7356  enmkvlem  7359  prubl  7705  letr  8261  eqord1  8662  prodge0  9033  lt2msq  9065  nnge1  9165  nzadd  9531  irradd  9879  irrmul  9880  xrletr  10042  frec2uzf1od  10667  zesq  10919  expcanlem  10976  nn0opthd  10983  bccmpl  11015  fundm2domnop0  11108  maxleast  11773  fisumss  11952  dvdsbnd  12526  prm2orodd  12697  coprm  12715  prmndvdsfaclt  12727  hashgcdeq  12811  cos11  15576  bj-nnsn  16329  bj-nnelirr  16548  ismkvnnlem  16656  nconstwlpolem  16669