Theorem con3d 640

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

This proof depends on syntax axioms:   -. wn 3   -> wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in1 623  ax-in2 624

This theorem is used by:  con3rr3  642  con3dimp  644  con3  651  nsyld  657  nsyli  658  jcn  661  notbi  676  impidc  870  bijadc  894  pm2.13dc  897  xoranor  1426  mo2n  2114  necon3ad  2462  necon3bd  2463  nelcon3d  2526  ssneld  3250  sscon  3363  difrab  3507  exmid1stab  4347  eunex  4710  ndmfvg  5729  suppssrst  6505  suppssrgst  6506  nnaord  6786  nnmord  6794  php5  7163  php5dom  7168  fidcen  7207  supmoti  7339  exmidomniim  7487  mkvprop  7504  enmkvlem  7507  prubl  7859  letr  8414  eqord1  8818  prodge0  9192  lt2msq  9224  nnge1  9336  nzadd  9708  irradd  10062  irrmul  10064  xrletr  10227  frec2uzf1od  10864  zesq  11117  expcanlem  11175  nn0opthd  11182  bccmpl  11214  fundm2domnop0  11322  maxleast  12002  fisumss  12184  dvdsbnd  12758  prm2orodd  12929  coprm  12948  prmndvdsfaclt  12960  nn0sqdcq  13013  hashgcdeq  13047  ballotfilemfc0  13290  ballotfilemfcc  13291  cos11  16081  logdivlt  16124  bposlem3  16313  bj-nnsn  16966  bj-nnelirr  17184  ismkvnnlem  17309  nconstwlpolem  17322