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  2110  necon3ad  2456  necon3bd  2457  nelcon3d  2520  ssneld  3244  sscon  3357  difrab  3499  exmid1stab  4326  eunex  4688  ndmfvg  5706  suppssrst  6474  suppssrgst  6475  nnaord  6755  nnmord  6763  php5  7125  php5dom  7130  fidcen  7169  supmoti  7297  exmidomniim  7445  mkvprop  7462  enmkvlem  7465  prubl  7817  letr  8372  eqord1  8774  prodge0  9145  lt2msq  9177  nnge1  9277  nzadd  9647  irradd  9996  irrmul  9997  xrletr  10160  frec2uzf1od  10792  zesq  11045  expcanlem  11102  nn0opthd  11109  bccmpl  11141  fundm2domnop0  11245  maxleast  11923  fisumss  12103  dvdsbnd  12677  prm2orodd  12848  coprm  12866  prmndvdsfaclt  12878  hashgcdeq  12962  ballotfilemfc0  13176  ballotfilemfcc  13177  cos11  15844  bj-nnsn  16631  bj-nnelirr  16849  ismkvnnlem  16963  nconstwlpolem  16977