Theorem con3d 140

Description: A contraposition deduction. Deduction form of con3 141. (Contributed by NM, 10-Jan-1993.)

Hypothesis

Ref	Expression
con3d.1	|- ( ph -> ( ps -> ch ) )

Assertion

Ref	Expression
con3d	|- ( ph -> ( -. ch -> -. ps ) )

Proof of Theorem con3d

Step	Hyp	Ref	Expression
1		notnot2 116	. . 3 |- ( -. -. ps -> ps )
2		con3d.1	. . 3 |- ( ph -> ( ps -> ch ) )
3	1, 2	syl5 32	. 2 |- ( ph -> ( -. -. ps -> ch ) )
4	3	con1d 129	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-3 8

This theorem is referenced by:  con3  141  con3rr3  143  nsyld  147  nsyli  148  mth8  151  pm2.52  160  pm5.21ndd  361  bija  362  con3dimp  448  stoic1a  1663  aleximi  1712  nelcon3d  2755  rexim  2849  spcimegf  3114  spcimedv  3119  rspcimedv  3138  ssneld  3420  sscon  3556  difrab  3708  eqoreldif  4004  dtru  4592  otiunsndisj  4707  wereu2  4836  nsuceq0  5510  ndmfv  5903  dff3  6050  soisores  6236  ressuppssdif  6955  wfrlem10  7063  tz7.49  7180  oaord  7266  oalimcl  7279  omord2  7286  omcan  7288  omeulem1  7301  oeord  7307  oecan  7308  nnaord  7338  nnmord  7351  nneob  7371  omsmo  7373  domtriord  7736  isinf  7803  pssnn  7808  frfi  7834  fisupg  7837  difinf  7859  supmo  7984  infmo  8029  fiinfg  8033  alephord  8524  fin17  8842  isfin7-2  8844  fin1a2lem12  8859  fpwwe2lem13  9085  prub  9437  genpnnp  9448  ltaddpr  9477  prlem936  9490  ltadd2  9756  ltord1  10161  prodge0  10474  ltmul1  10477  lt2msq  10513  nnge1  10657  zeo  11044  irradd  11311  irrmul  11312  mul2lt0bi  11425  supxrun  11626  supxrgtmnf  11640  ssfzoulel  12034  zesq  12433  bccmpl  12532  repswswrd  12941  lcmftp  14688  coprm  14736  prmreclem3  14941  vdwnnlem2  15025  latnlej2  16395  mgm2nsgrplem3  16732  f1omvdco2  17167  oddvds  17274  gexdvds  17313  frgpnabl  17589  ablfac1eulem  17783  ablfac1eu  17784  psgnodpm  19233  obselocv  19368  1marepvmarrepid  19677  mdetunilem9  19722  t1conperf  20528  txindislem  20725  fbasrn  20977  isufil2  21001  ufileu  21012  filufint  21013  ufilen  21023  fin1aufil  21025  alexsubALTlem4  21143  ptcmplem2  21146  itg2gt0  22797  cosord  23560  argimgt0  23640  logdivlt  23649  logrec  23779  dcubic  23851  wilthlem2  24073  bposlem3  24293  dchrisum0fno1  24428  usgranloop0  25186  nbgra0nb  25236  nbcusgra  25270  cusgrafi  25289  vdusgra0nedg  25715  usgravd0nedg  25725  usgravd00  25726  2spotmdisj  25875  chnlen0  27178  staddi  27980  stadd3i  27982  strlem1  27984  atoml2i  28117  psgnfzto1stlem  28687  madjusmdetlem1  28727  madjusmdetlem2  28728  hasheuni  28980  sitgaddlemb  29254  eulerpartlemb  29274  ballotlemfc0  29398  ballotlemfcc  29399  dfon2lem6  30505  exnel  30520  sltres  30622  nodenselem4  30644  nofulllem5  30666  nn0prpwlem  31049  waj-ax  31145  bj-dtru  31478  sucneqond  31838  wl-ax11-lem3  31981  poimirlem26  32030  poimirlem28  32032  poimirlem31  32035  areacirc  32101  pridlc3  32370  lkreqN  32807  atlrelat1  32958  2llnneN  33045  cdlemg4c  34250  mapdh8e  35423  hashgcdeq  36146  vk15.4j  36955  isosctrlem1ALT  37394  afvres  38819  otiunsndisjX  39152  fundmge2nop  39172  nbumgr  39579  uhgrnbgr0nb  39586  cusgrfi  39684  vtxduhgr0nedg  39715  uhgrvd00  39757  1wlkp1lem6  39874  copisnmnd  40317  dig1  40927