Theorem con3d 596

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 594	. . 3 |- ( ch -> -. -. ch )
3	1, 2	syl6 33	. 2 |- ( ph -> ( ps -> -. -. ch ) )
4	3	con2d 589	1 |- ( ph -> ( -. ch -> -. ps ) )

Syntax hints:   -. wn 3   -> wi 4

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-in1 579  ax-in2 580

This theorem is referenced by:  con3rr3  598  con3dimp  599  con3  606  nsyld  612  nsyli  613  mth8  614  notbid  627  impidc  793  bijadc  814  pm2.13dc  817  xoranor  1313  mo2n  1976  necon3ad  2297  necon3bd  2298  ssneld  3027  sscon  3134  difrab  3273  eunex  4377  ndmfvg  5335  nnaord  6266  nnmord  6274  php5  6572  php5dom  6577  supmoti  6686  exmidomniim  6795  prubl  7043  letr  7566  eqord1  7959  prodge0  8313  lt2msq  8345  nnge1  8443  nzadd  8800  irradd  9129  irrmul  9130  xrletr  9271  frec2uzf1od  9809  zesq  10068  expcanlem  10120  nn0opthd  10126  bccmpl  10158  maxleast  10642  fisumss  10780  efler  10985  dvdsbnd  11222  prm2orodd  11382  coprm  11397  prmndvdsfaclt  11409  hashgcdeq  11478  bj-notbi  11771  bj-nnelirr  11803