Theorem con3d 634

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 632	. . 3 |- ( ch -> -. -. ch )
3	1, 2	syl6 33	. 2 |- ( ph -> ( ps -> -. -. ch ) )
4	3	con2d 627	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 617  ax-in2 618

This theorem is referenced by:  con3rr3  636  con3dimp  638  con3  645  nsyld  651  nsyli  652  jcn  655  notbi  670  impidc  863  bijadc  887  pm2.13dc  890  xoranor  1419  mo2n  2105  necon3ad  2442  necon3bd  2443  nelcon3d  2506  ssneld  3227  sscon  3339  difrab  3479  exmid1stab  4296  eunex  4657  ndmfvg  5666  nnaord  6672  nnmord  6680  php5  7039  php5dom  7044  fidcen  7081  supmoti  7183  exmidomniim  7331  mkvprop  7348  enmkvlem  7351  prubl  7696  letr  8252  eqord1  8653  prodge0  9024  lt2msq  9056  nnge1  9156  nzadd  9522  irradd  9870  irrmul  9871  xrletr  10033  frec2uzf1od  10658  zesq  10910  expcanlem  10967  nn0opthd  10974  bccmpl  11006  fundm2domnop0  11099  maxleast  11764  fisumss  11943  dvdsbnd  12517  prm2orodd  12688  coprm  12706  prmndvdsfaclt  12718  hashgcdeq  12802  cos11  15567  bj-nnsn  16265  bj-nnelirr  16484  ismkvnnlem  16592  nconstwlpolem  16605