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  866  bijadc  890  pm2.13dc  893  xoranor  1422  mo2n  2107  necon3ad  2445  necon3bd  2446  nelcon3d  2509  ssneld  3230  sscon  3343  difrab  3483  exmid1stab  4304  eunex  4665  ndmfvg  5679  suppssrst  6439  suppssrgst  6440  nnaord  6720  nnmord  6728  php5  7087  php5dom  7092  fidcen  7131  supmoti  7235  exmidomniim  7383  mkvprop  7400  enmkvlem  7403  prubl  7749  letr  8304  eqord1  8705  prodge0  9076  lt2msq  9108  nnge1  9208  nzadd  9576  irradd  9924  irrmul  9925  xrletr  10087  frec2uzf1od  10714  zesq  10966  expcanlem  11023  nn0opthd  11030  bccmpl  11062  fundm2domnop0  11158  maxleast  11836  fisumss  12016  dvdsbnd  12590  prm2orodd  12761  coprm  12779  prmndvdsfaclt  12791  hashgcdeq  12875  cos11  15647  bj-nnsn  16434  bj-nnelirr  16652  ismkvnnlem  16768  nconstwlpolem  16781