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  3185  sscon  3297  difrab  3437  exmid1stab  4241  eunex  4597  ndmfvg  5589  nnaord  6567  nnmord  6575  php5  6919  php5dom  6924  supmoti  7059  exmidomniim  7207  mkvprop  7224  enmkvlem  7227  prubl  7553  letr  8109  eqord1  8510  prodge0  8881  lt2msq  8913  nnge1  9013  nzadd  9378  irradd  9720  irrmul  9721  xrletr  9883  frec2uzf1od  10498  zesq  10750  expcanlem  10807  nn0opthd  10814  bccmpl  10846  maxleast  11378  fisumss  11557  dvdsbnd  12123  prm2orodd  12294  coprm  12312  prmndvdsfaclt  12324  hashgcdeq  12408  cos11  15089  bj-nnsn  15379  bj-nnelirr  15599  ismkvnnlem  15696  nconstwlpolem  15709