Theorem con3d 139

Description: A contraposition deduction. Deduction form of con3 140. (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 33	. 2 |- ( ph -> ( -. -. ps -> ch ) )
4	3	con1d 128	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  140  con3rr3  142  nsyld  146  nsyli  147  mth8  150  pm2.52  159  pm5.21ndd  356  bija  357  con3dimp  443  stoic1a  1655  aleximi  1704  nelcon3d  2736  rexim  2852  spcimegf  3128  spcimedv  3133  rspcimedv  3152  ssneld  3434  sscon  3567  difrab  3717  eqoreldif  4013  dtru  4594  otiunsndisj  4707  wereu2  4831  nsuceq0  5503  ndmfv  5889  dff3  6035  soisores  6218  ressuppssdif  6936  wfrlem10  7045  tz7.49  7162  oaord  7248  oalimcl  7261  omord2  7268  omcan  7270  omeulem1  7283  oeord  7289  oecan  7290  nnaord  7320  nnmord  7333  nneob  7353  omsmo  7355  domtriord  7718  isinf  7785  pssnn  7790  frfi  7816  fisupg  7819  difinf  7841  supmo  7966  infmo  8011  fiinfg  8015  alephord  8506  fin17  8824  isfin7-2  8826  fin1a2lem12  8841  fpwwe2lem13  9067  prub  9419  genpnnp  9430  ltaddpr  9459  prlem936  9472  ltadd2  9738  ltord1  10140  prodge0  10452  ltmul1  10455  lt2msq  10491  nnge1  10635  zeo  11021  irradd  11288  irrmul  11289  mul2lt0bi  11402  supxrun  11601  supxrgtmnf  11615  ssfzoulel  12005  zesq  12395  bccmpl  12494  repswswrd  12887  lcmftp  14609  coprm  14657  prmreclem3  14862  vdwnnlem2  14946  latnlej2  16317  mgm2nsgrplem3  16654  f1omvdco2  17089  oddvds  17196  gexdvds  17235  frgpnabl  17511  ablfac1eulem  17705  ablfac1eu  17706  psgnodpm  19156  obselocv  19291  1marepvmarrepid  19600  mdetunilem9  19645  t1conperf  20451  txindislem  20648  fbasrn  20899  isufil2  20923  ufileu  20934  filufint  20935  ufilen  20945  fin1aufil  20947  alexsubALTlem4  21065  ptcmplem2  21068  itg2gt0  22718  cosord  23481  argimgt0  23561  logdivlt  23570  logrec  23700  dcubic  23772  wilthlem2  23994  bposlem3  24214  dchrisum0fno1  24349  usgranloop0  25107  nbgra0nb  25157  nbcusgra  25191  cusgrafi  25210  vdusgra0nedg  25636  usgravd0nedg  25646  usgravd00  25647  2spotmdisj  25796  chnlen0  27097  staddi  27899  stadd3i  27901  strlem1  27903  atoml2i  28036  psgnfzto1stlem  28613  madjusmdetlem1  28653  madjusmdetlem2  28654  hasheuni  28906  sitgaddlemb  29181  eulerpartlemb  29201  ballotlemfc0  29325  ballotlemfcc  29326  dfon2lem6  30434  exnel  30449  sltres  30551  nodenselem4  30573  nofulllem5  30595  nn0prpwlem  30978  waj-ax  31074  bj-dtru  31412  sucneqond  31768  wl-ax11-lem3  31917  poimirlem26  31966  poimirlem28  31968  poimirlem31  31971  areacirc  32037  pridlc3  32306  lkreqN  32736  atlrelat1  32887  2llnneN  32974  cdlemg4c  34179  mapdh8e  35352  hashgcdeq  36075  vk15.4j  36885  isosctrlem1ALT  37331  afvres  38674  otiunsndisjX  39006  fundmge2nop  39026  nbumgr  39415  uhgrnbgr0nb  39422  cusgrfi  39519  vtxduhgr0nedg  39546  uhgrvd00  39571  copisnmnd  39862  dig1  40472