MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3adant1 Unicode version

Theorem 3adant1 975
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.)
Hypothesis
Ref Expression
3adant.1  |-  ( (
ph  /\  ps )  ->  ch )
Assertion
Ref Expression
3adant1  |-  ( ( th  /\  ph  /\  ps )  ->  ch )

Proof of Theorem 3adant1
StepHypRef Expression
1 3simpc 956 . 2  |-  ( ( th  /\  ph  /\  ps )  ->  ( ph  /\ 
ps ) )
2 3adant.1 . 2  |-  ( (
ph  /\  ps )  ->  ch )
31, 2syl 16 1  |-  ( ( th  /\  ph  /\  ps )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  3ad2ant2  979  3ad2ant3  980  rsp2e  2729  sbciegft  3151  reuhyp  4710  ordunel  4766  breldmg  5034  funopg  5444  fex2  5562  fvun1  5753  fnreseql  5799  ftpg  5875  mpt2eq3ia  6098  poxp  6417  smores3  6574  oaord  6749  oacan  6750  oaword  6751  omord  6770  omcan  6771  omwordri  6774  odi  6781  omass  6782  oeord  6790  oecan  6791  oewordri  6794  oeordsuc  6796  nnaord  6821  nnaordr  6822  nndi  6825  nnmass  6826  nnaword  6829  nnmord  6834  nnmwordri  6838  erov  6960  ecopovtrn  6966  ixpf  7043  mapxpen  7232  fimax2g  7312  unbnn  7322  inelfi  7381  elfiun  7393  suppr  7429  r111  7657  dif1card  7848  xpcdaen  8019  mapcdaen  8020  ackbij1lem16  8071  cff1  8094  cfflb  8095  cfsmolem  8106  fin23lem34  8182  hsmexlem2  8263  axcc3  8274  domtriomlem  8278  axdc3lem4  8289  axdc4lem  8291  axcclem  8293  konigthlem  8399  gchdomtri  8460  tskpr  8601  tskop  8602  tskuni  8614  tskun  8617  gruop  8636  gruun  8637  grudomon  8648  adderpqlem  8787  mulerpqlem  8788  addassnq  8791  mulassnq  8792  distrnq  8794  ltsonq  8802  ltanq  8804  ltmnq  8805  genpass  8842  distrlem1pr  8858  distrlem4pr  8859  ltsopr  8865  adddir  9039  axlttrn  9104  ltletr  9122  letr  9123  mul32  9189  mul31  9190  add32  9236  subsub23  9266  addsubass  9271  subcan2  9282  subsub2  9285  nppcan2  9288  sub32  9291  nnncan  9292  nnncan2  9294  pnpcan2  9297  subdi  9423  subdir  9424  receu  9623  divmul3  9639  divrec  9650  divrec2  9651  divsubdir  9666  divdiv1  9681  redivcl  9689  div2neg  9693  ltmul2  9817  lemul1  9818  lemul2  9819  lemul2a  9821  lediv1  9831  gt0div  9832  ge0div  9833  ltdivmul  9838  ledivmul  9839  ledivmulOLD  9840  ltdivmul2  9841  ledivmul2  9843  ledivmul2OLD  9844  lemuldiv  9845  ltdiv23  9857  lediv23  9858  ledivp1i  9892  ltdivp1i  9893  uzind2  10318  nn0ind  10322  fnn0ind  10325  xrltletr  10703  xrletr  10704  xrre2  10714  xrltmin  10726  xrlemin  10728  xleadd2a  10789  xleadd1  10790  xltadd2  10792  xmulasslem3  10821  xmulass  10822  xltmul2  10828  ixxdisj  10887  iooneg  10973  iccneg  10974  icoshft  10975  icoshftf1o  10976  icodisj  10978  snunioo  10979  fzen  11028  fzrev3  11067  fzoaddel2  11131  modcyc  11231  modcyc2  11232  moddi  11239  modsubdir  11240  expdiv  11385  digit2  11467  brfi1uzind  11670  ccatass  11705  swrdval  11719  ccatco  11759  shftval2  11845  mulre  11881  absdiv  12055  absdiflt  12076  absdifle  12077  abs3dif  12090  cau3  12114  ello12r  12266  elo12r  12277  geoisum1c  12612  rpnnen2lem4  12772  rpnnen2lem7  12775  dvdsmulc  12832  dvdsmulcr  12834  dvdsmultr1  12839  dvdsmultr2  12840  dvdssub2  12842  oexpneg  12866  divalgb  12879  ndvdsadd  12883  sadass  12938  modgcd  12991  dvdsgcd  12998  dvdsgcdb  12999  gcdass  13000  mulgcd  13001  absmulgcd  13002  rpmulgcd  13010  nn0seqcvgd  13016  algcvga  13025  coprmdvds  13057  coprmdvds2  13058  rpmul  13078  qnumdenbi  13091  coprimeprodsq  13138  pythagtriplem4  13148  pythagtriplem8  13152  pythagtriplem9  13153  pythagtriplem12  13155  pythagtriplem14  13157  pythagtriplem16  13159  pcpremul  13172  pcgcd  13206  vdwapval  13296  vdwapun  13297  mreiincl  13776  mreincl  13779  mremre  13784  mrcss  13796  catcisolem  14216  pleval2  14377  pospo  14385  clatl  14498  lubss  14503  lubun  14505  clatglbss  14509  ipole  14539  ipolt  14540  pslem  14593  dirtr  14636  gsumws2  14743  frmdmnd  14759  isgrpi  14786  grpsubrcan  14825  grpinvsub  14826  grpsubeq0  14830  grpnpcan  14835  divssub  14955  ghmsub  14969  symggrp  15058  lsmass  15257  efgsrel  15321  cntzcmn  15414  dvrcl  15746  unitdvcl  15747  dvrcan1  15751  subrgmre  15847  abvsubtri  15878  abvtrivd  15883  lmodvsubval2  15954  lss0cl  15978  lssintcl  15995  lssincl  15996  reslmhm2  16084  lspvadd  16123  lspsntrim  16125  islbs3  16182  rrgeq0  16305  cncrng  16677  xrsmcmn  16679  cndrng  16685  cnsrng  16690  xrs1mnd  16691  absabv  16711  unopn  16931  clsss  17073  cldmre  17097  toponmre  17112  opnssneib  17134  restabs  17183  restcls  17199  restntr  17200  hausnei2  17371  cmpsublem  17416  hausmapdom  17516  ptpjcn  17596  upxp  17608  ptrescn  17624  xkopjcn  17641  fbssfi  17822  snfil  17849  ufprim  17894  rnelfm  17938  flimrest  17968  fclsrest  18009  tmdgsum  18078  blpnfctr  18419  mscl  18444  xmscl  18445  xmsge0  18446  xmseq0  18447  restmetu  18570  ngpds  18603  unitnmn0  18657  xrsxmet  18793  metds0  18833  cncfmptc  18894  cphsqrcl  19100  cfil3i  19175  cfilres  19202  cmmbl  19382  voliunlem2  19398  itg2ub  19578  itgrecl  19642  evlsval2  19894  tdeglem3  19935  r1pid  20035  efgh  20396  eflogeq  20449  cxpadd  20523  lawcos  20611  pythag  20612  asinsinb  20690  acoscosb  20691  atantanb  20717  amgmlem  20781  lgsneg  21056  lgsne0  21070  nb3graprlem2  21414  cusgra3v  21426  cusgrasizeindslem3  21437  sizeusglecusglem2  21447  usgrnloop  21516  spthonepeq  21540  constr2spth  21553  constr2pth  21554  redwlk  21559  cyclispthon  21573  usgrcyclnl1  21580  usgrcyclnl2  21581  3v3e3cycl1  21584  constr3lem5  21588  constr3trllem2  21591  constr3pthlem2  21596  4cycl4v4e  21606  4cycl4dv4e  21608  vdgrfval  21619  gxnn0suc  21805  issubgoi  21851  ablomul  21896  imsmetlem  22135  nmoxr  22220  nmoolb  22225  blometi  22257  phpar2  22277  phpar  22278  ipasslem5  22289  hvadd32  22489  hvaddsub12  22493  hvaddsubass  22496  hvsubass  22499  hvsub32  22500  hvsubdistr1  22504  hvsubdistr2  22505  hvmulcan  22527  hvmulcan2  22528  hvsubcan  22529  his5  22541  his2sub  22547  hhssnv  22717  shlej2  22816  pjoi0  23172  hodcl  23203  hoadd32  23239  hosubdi  23264  hosubsub2  23268  hoaddsubass  23271  hosubsub4  23274  nmoplb  23363  unop  23371  hmop  23378  nmfnlb  23380  lnopmul  23423  kbass1  23572  kbass2  23573  leopmul2i  23591  leoptr  23593  cvntr  23748  mdslmd4i  23789  mdexchi  23791  atcv1  23836  sumdmdii  23871  xreceu  24121  isinftm  24204  unitdivcld  24252  logblt  24359  esummulc1  24424  hasheuni  24428  unelsiga  24470  cvmsf1o  24912  cvmscld  24913  modaddabs  25068  lediv2aALT  25070  mulcan1g  25142  mulcan2g  25143  mulsuble0b  25146  subdivcomb2  25149  gcd32  25318  fununiq  25340  trpredpo  25452  poseq  25467  wfr3g  25469  frr3g  25494  sltres  25532  nocvxmin  25559  dfrdg4  25703  brbtwn2  25748  colinearalg  25753  eleesubd  25755  axcgrrflx  25757  axcgrtr  25758  axsegcon  25770  ax5seglem1  25771  ax5seglem2  25772  ax5seglem4  25775  axbtwnid  25782  axlowdimlem14  25798  axlowdim  25804  axcontlem5  25811  axcontlem7  25813  brcolinear  25897  colinearex  25898  cnambfre  26154  nn0prpwlem  26215  clsun  26221  fnemeet1  26285  fnemeet2  26286  fnejoin1  26287  fnejoin2  26288  eltail  26293  cocanfo  26309  f1ocan1fv  26318  metf1o  26351  ismtybnd  26406  ghomco  26448  isdrngo2  26464  inidl  26530  igenmin  26564  mapco2g  26659  mzpcompact2lem  26698  eqrabdioph  26726  lerabdioph  26755  eluzrabdioph  26756  ltrabdioph  26758  nerabdioph  26759  dvdsrabdioph  26760  reglogcl  26843  rmxyadd  26874  rmyabs  26913  congadd  26921  congabseq  26929  rmydioph  26975  uvcresum  27110  lindfmm  27165  lindsmm  27166  symggen  27279  mendrng  27368  mendlmod  27369  dvconstbi  27419  fmul01  27577  stoweidlem60  27676  stowei  27680  sigarls  27714  f13dfv  27962  swrdnd  28001  swrd0swrd  28009  swrdswrdlem  28010  swrdccatin2  28018  swrdccatin12lem3a  28021  swrdccatin12lem3b  28022  swrdccatin12lem3c  28023  swrdccatin12  28026  swrdccatin12c  28028  swrdccat3  28029  swrdccat3a  28030  swrdccat3b  28031  usgra2pthspth  28035  el2spthonot  28067  el2spthonot0  28068  usg2wlkonot  28080  frgra3v  28106  3vfriswmgra  28109  frgrawopreg  28152  frg2woteu  28158  frgregordn0  28173  bnj545  28972  bnj594  28989  bnj1311  29099  lubunNEW  29456  cmtvalN  29694  cvrval  29752  pmapmeet  30255  paddval  30280  paddssat  30296  elpcliN  30375  pclssN  30376  pclunN  30380  paddunN  30409  poldmj1N  30410  tendoplcl2  31260  tendoplcl  31263  dihmeet  31826
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator