Theorem con3d 621

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

This theorem is referenced by:  con3rr3  623  con3dimp  625  con3  632  nsyld  638  nsyli  639  jcn  641  notbi  656  impidc  848  bijadc  872  pm2.13dc  875  xoranor  1367  mo2n  2042  necon3ad  2378  necon3bd  2379  nelcon3d  2442  ssneld  3144  sscon  3256  difrab  3396  eunex  4538  ndmfvg  5517  nnaord  6477  nnmord  6485  php5  6824  php5dom  6829  supmoti  6958  exmidomniim  7105  mkvprop  7122  enmkvlem  7125  prubl  7427  letr  7981  eqord1  8381  prodge0  8749  lt2msq  8781  nnge1  8880  nzadd  9243  irradd  9584  irrmul  9585  xrletr  9744  frec2uzf1od  10341  zesq  10573  expcanlem  10628  nn0opthd  10635  bccmpl  10667  maxleast  11155  fisumss  11333  dvdsbnd  11889  prm2orodd  12058  coprm  12076  prmndvdsfaclt  12088  hashgcdeq  12171  cos11  13414  bj-nnsn  13614  bj-nnelirr  13835  exmid1stab  13880  ismkvnnlem  13931  nconstwlpolem  13943