Theorem con3d 632

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 630	. . 3 |- ( ch -> -. -. ch )
3	1, 2	syl6 33	. 2 |- ( ph -> ( ps -> -. -. ch ) )
4	3	con2d 625	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 615  ax-in2 616

This theorem is referenced by:  con3rr3  634  con3dimp  636  con3  643  nsyld  649  nsyli  650  jcn  652  notbi  667  impidc  859  bijadc  883  pm2.13dc  886  xoranor  1388  mo2n  2073  necon3ad  2409  necon3bd  2410  nelcon3d  2473  ssneld  3186  sscon  3298  difrab  3438  exmid1stab  4242  eunex  4598  ndmfvg  5592  nnaord  6576  nnmord  6584  php5  6928  php5dom  6933  supmoti  7068  exmidomniim  7216  mkvprop  7233  enmkvlem  7236  prubl  7570  letr  8126  eqord1  8527  prodge0  8898  lt2msq  8930  nnge1  9030  nzadd  9395  irradd  9737  irrmul  9738  xrletr  9900  frec2uzf1od  10515  zesq  10767  expcanlem  10824  nn0opthd  10831  bccmpl  10863  maxleast  11395  fisumss  11574  dvdsbnd  12148  prm2orodd  12319  coprm  12337  prmndvdsfaclt  12349  hashgcdeq  12433  cos11  15173  bj-nnsn  15463  bj-nnelirr  15683  ismkvnnlem  15783  nconstwlpolem  15796