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

Theorem 3ad2ant3 980
Description: Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)
Hypothesis
Ref Expression
3ad2ant.1  |-  ( ph  ->  ch )
Assertion
Ref Expression
3ad2ant3  |-  ( ( ps  /\  th  /\  ph )  ->  ch )

Proof of Theorem 3ad2ant3
StepHypRef Expression
1 3ad2ant.1 . . 3  |-  ( ph  ->  ch )
21adantl 453 . 2  |-  ( ( th  /\  ph )  ->  ch )
323adant1 975 1  |-  ( ( ps  /\  th  /\  ph )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936
This theorem is referenced by:  simp3l  985  simp3r  986  simp31  993  simp32  994  simp33  995  simp3ll  1028  simp3lr  1029  simp3rl  1030  simp3rr  1031  simp3l1  1062  simp3l2  1063  simp3l3  1064  simp3r1  1065  simp3r2  1066  simp3r3  1067  simp31l  1080  simp31r  1081  simp32l  1082  simp32r  1083  simp33l  1084  simp33r  1085  simp311  1104  simp312  1105  simp313  1106  simp321  1107  simp322  1108  simp323  1109  simp331  1110  simp332  1111  simp333  1112  3anim123i  1139  3jaao  1251  ceqsalt  2938  ceqsralt  2939  vtoclgft  2962  tpssi  3925  prnebg  3939  epne3  4720  limsuc  4788  poltletr  5228  funprg  5459  funtpg  5460  fntpg  5465  ftpg  5875  fsnunf  5890  fsnunfv  5892  fvpr1g  5896  fvpr2g  5897  fnsuppres  5911  weniso  6034  smoel  6581  smoord  6586  omwordi  6773  oneo  6783  oeord  6790  oewordi  6793  nnmwordi  6837  nnneo  6853  uniinqs  6943  undifixp  7057  domss2  7225  domssex2  7226  unxpdomlem3  7274  dif1enOLD  7299  dif1en  7300  dffi2  7386  unwdomg  7508  ixpiunwdom  7515  oemapvali  7596  en3lplem1  7626  fodomfi2  7897  infcdaabs  8042  infunabs  8043  infdif  8045  ackbij1lem9  8064  ackbij1lem16  8071  coflim  8097  cfsmolem  8106  isfin2-2  8155  fin1a2lem9  8244  hsmexlem2  8263  axcc2lem  8272  axcc3  8274  domtriomlem  8278  axdc3lem4  8289  axcclem  8293  zornn0g  8341  axacndlem4  8441  axacndlem5  8442  axacnd  8443  gchdomtri  8460  fpwwe  8477  tskssel  8588  tskint  8616  tskurn  8620  gruurn  8629  gruixp  8640  grudomon  8648  gruina  8649  adderpqlem  8787  mulerpqlem  8788  addassnq  8791  mulassnq  8792  distrnq  8794  ltsonq  8802  ltanq  8804  ltmnq  8805  reclem3pr  8882  addid2  9205  addcan2  9207  divdir  9657  divcan5  9672  ltdiv1  9830  infmrcl  9943  infmrlb  9945  lt2halves  10158  zdivmul  10298  xaddass  10784  xleadd1  10790  xltadd1  10791  xmulasslem3  10821  xmulass  10822  xlemul1  10825  xlemul2  10826  xltmul1  10827  xadddir  10831  elioo5  10924  iccsupr  10953  iccneg  10974  icoshft  10975  icoshftf1o  10976  iccsplit  10985  fzen  11028  fzrevral  11086  fzshftral  11089  elfzo  11097  modabs  11229  modcyc  11231  moddi  11239  modsubdir  11240  expdiv  11385  leexp2a  11390  bcval3  11552  hashnnn0genn0  11582  hashgadd  11606  hashunx  11615  hashtpg  11646  hashfun  11655  brfi1indlem  11669  ccatval1  11700  ccatval2  11701  ccatval3  11702  ccatass  11705  swrdval2  11722  splval  11735  ccatco  11759  f1oun2prg  11819  swrds2  11835  sqr0  12002  elicc4abs  12078  mulcn2  12344  demoivreALT  12757  rpnnen2lem4  12772  dvdsval2  12810  dvdsexp  12860  mulgcd  13001  mulgcdr  13003  gcddiv  13004  rpmulgcd  13010  rplpwr  13011  prmexpb  13072  rpexp  13075  coprimeprodsq  13138  pythagtriplem1  13145  pythagtriplem3  13147  pythagtriplem10  13149  pythagtriplem6  13150  pythagtriplem11  13154  pythagtriplem12  13155  pythagtriplem13  13156  pythagtriplem15  13158  pythagtriplem17  13160  pythagtriplem19  13162  pcdvdsb  13197  pcfaclem  13222  vdwapun  13297  ramval  13331  0ram2  13344  0ramcl  13346  imasaddvallem  13709  imasvscaval  13718  mreiincl  13776  mremre  13784  mrieqv2d  13819  cofurid  14043  xpcpropd  14260  clatleglb  14508  gsumccat  14742  mulgdirlem  14869  mulgp1  14871  eqglact  14946  mndodcongi  15136  oddvdsnn0  15137  odngen  15166  gexnnod  15177  lsmlub  15252  lsmass  15257  efgsval2  15320  efgsrel  15321  ghmplusg  15416  odadd1  15418  odadd2  15419  gsumsn  15498  dvrcan1  15751  dvrcan3  15752  irredrmul  15767  srngadd  15900  srngmul  15901  lmhmvsca  16076  reslmhm2  16084  lbspss  16109  lsmsp  16113  lspsneu  16150  lidldvgen  16281  psropprmul  16587  coe1add  16612  coe1addfv  16613  coe1subfv  16614  coe1tm  16620  coe1sclmul  16629  coe1sclmul2  16631  cssmre  16875  iuncld  17064  clsss  17073  ntrcls0  17095  iscldtop  17114  neiss  17128  neips  17132  restcldi  17191  cnpnei  17282  cnconst2  17301  cnpresti  17306  sslm  17317  cnt0  17364  cnt1  17368  cnhaus  17372  cncmp  17409  cmpcld  17419  cnconn  17438  concompss  17449  elptr  17558  upxp  17608  qtoptop2  17684  ordthmeolem  17786  opnfbas  17827  isfil2  17841  fbasweak  17850  snfbas  17851  fgss  17858  fgcl  17863  fbasrn  17869  trnei  17877  cfinfil  17878  csdfil  17879  supfil  17880  filufint  17905  fin1aufil  17917  fmval  17928  fmf  17930  elfm  17932  elfm3  17935  imaelfm  17936  rnelfmlem  17937  rnelfm  17938  flimclslem  17969  flfneii  17977  cnpfcfi  18025  alexsubALT  18035  ptcmplem3  18038  ustref  18201  ustelimasn  18205  utop3cls  18234  ressusp  18248  cfiluexsm  18273  prdsxmetlem  18351  txmetcn  18531  nmmtri  18621  nmrtri  18623  unitnmn0  18657  nminvr  18658  nmotri  18726  nghmplusg  18727  isclmi  19055  fmcfil  19178  srabn  19267  itgconst  19663  dvn2bss  19769  evlsval  19893  evlsval2  19894  deg1mul3  19991  deg1mul3le  19992  deg1tmle  19993  q1peqb  20030  r1pcl  20033  r1pdeglt  20034  r1pid  20035  dvdsq1p  20036  dvdsr1p  20037  ptolemy  20357  sincosq1eq  20373  logmul2  20464  logdiv2  20465  cxplt2  20542  pythag  20612  bcmono  21014  efexple  21018  lgsdirnn0  21076  selberglem3  21194  nbgraf1olem1  21404  nbusgrafi  21411  nb3graprlem1  21413  nb3graprlem2  21414  cusgra2v  21424  cusgra3v  21426  2trllemH  21505  2trllemE  21506  constr1trl  21541  constr2spthlem1  21547  2pthlem2  21549  2wlklem1  21550  2pthon  21555  constr3lem4  21587  constr3trllem2  21591  constr3trllem5  21594  constr3pthlem2  21596  vdgrfival  21621  vdgrf  21622  vdgrfif  21623  vdusgra0nedg  21632  hashnbgravd  21634  gxpval  21800  gxnval  21801  gxnn0neg  21804  gxnn0suc  21805  gxneg  21807  gxsuc  21813  gxnn0add  21815  gxadd  21816  gxsub  21817  gxnn0mul  21818  gxmul  21819  gxmodid  21820  gxdi  21837  zerdivemp1  21975  rngoridfz  21976  vcid  21983  vcdi  21984  vcdir  21985  vcass  21986  imsmetlem  22135  0oval  22242  ajval  22316  shlub  22869  hmopco  23479  adjlnop  23542  mdslmd4i  23789  divnumden2  24114  ress0g  24135  ressnm  24137  ofldadd  24191  ofldmul  24192  pstmfval  24244  logeq0im1  24347  ind1  24369  ind0  24370  sigaclcuni  24454  sigagenss2  24486  measun  24518  measvuni  24521  dya2iocnrect  24584  ballotlemieq  24727  ballotlemrv1  24731  lgamgulmlem1  24766  erdszelem2  24831  cnpcon  24870  cvmscld  24913  ghomf1olem  25058  dedekind  25140  prodfrec  25176  ntrivcvgfvn0  25180  iprodefisumlem  25270  binomrisefac  25309  dvdspw  25317  dfon2lem3  25355  dfon2lem7  25359  predpo  25398  frrlem4  25498  nofulllem3  25572  brbtwn2  25748  axcgrid  25759  ax5seglem1  25771  ax5seglem2  25772  ax5seg  25781  axpasch  25784  axlowdimlem16  25800  axcontlem7  25813  btwndiff  25865  brcolinear2  25896  btwnconn1  25939  nnssi3  26110  nndivsub  26111  areacirclem4  26183  areacirclem6  26186  areacirc  26187  nn0prpwlem  26215  hmeoclda  26226  hmeocldb  26227  ivthALT  26228  ssref  26253  fnemeet1  26285  fnejoin1  26287  upixp  26321  filbcmb  26332  cnresima  26363  smprngopr  26552  igenval2  26566  ismrcd1  26642  istopclsd  26644  ismrc  26645  mapfzcons  26662  eldioph2  26710  diophrex  26724  diophren  26764  pellexlem1  26782  pellexlem5  26786  pellqrexplicit  26830  reglogmul  26846  reglogexp  26847  rmxycomplete  26870  congmul  26922  congabseq  26929  acongsym  26931  acongneg2  26932  fzneg  26937  acongeq  26938  jm2.19  26954  jm2.22  26956  jm2.23  26957  jm2.20nn  26958  rmydioph  26975  rmxdiophlem  26976  jm3.1  26981  pwssplit3  27058  pwssplit4  27059  frlmup4  27121  enfixsn  27125  mapfien2  27126  islindf2  27152  lindsind2  27157  f1lindf  27160  lindsss  27162  f1linds  27163  lindsmm  27166  lbslcic  27179  hbtlem2  27196  mndvcl  27314  mndvass  27315  mhmvlin  27320  idomrootle  27379  dvconstbi  27419  expgrowth  27420  fmul01lt1lem1  27581  climsuselem1  27600  climsuse  27601  stoweidlem3  27619  stoweidlem16  27632  stoweidlem17  27633  stoweidlem26  27642  stoweidlem34  27650  stoweidlem57  27673  el2xptp0  27949  oteqimp  27951  otthg  27952  ssfz12  27976  elfzelfzelfz  27981  swrd0swrd  28009  swrdswrdlem  28010  swrdswrd  28011  swrdccatin2  28018  swrdccatin12lem3c  28023  swrdccatin12lem3  28024  swrdccatin12  28026  swrdccatin12b  28027  swrdccat3b  28031  usgra2pth  28041  el2wlkonot  28066  el2spthonot  28067  el2spthonot0  28068  el2wlkonotot0  28069  3vfriswmgralem  28108  3vfriswmgra  28109  2spotdisj  28164  usg2spot2nb  28168  chordthmALT  28755  bnj837  28836  bnj517  28962  bnj553  28975  bnj594  28989  bnj967  29022  bnj1097  29056  bnj1110  29057  bnj1118  29059  bnj1128  29065  bnj1125  29067  bnj1145  29068  bnj1136  29072  bnj1173  29077  bnj1189  29084  bnj1204  29087  bnj1279  29093  bnj1321  29102  bnj1413  29110  lsmsat  29491  lsmsatcv  29493  lsatcvatlem  29532  islshpcv  29536  l1cvpat  29537  lfli  29544  lshpset2N  29602  cvrnbtwn  29754  meetat2  29780  atcmp  29794  atcvreq0  29797  atlatmstc  29802  cvlcvr1  29822  cvlcvrp  29823  cvlatcvr2  29825  cvr2N  29893  cvratlem  29903  2atjm  29927  athgt  29938  2lplnmN  30041  2llnmj  30042  2lplnmj  30104  dalemswapyzps  30172  dalem23  30178  dalem24  30179  dalem25  30180  dalem27  30181  dalem28  30182  dalem38  30192  dalem39  30193  dalem44  30198  dalem45  30199  dalem51  30205  dalem52  30206  dalem56  30210  pmapglbx  30251  pmapjat1  30335  pmapjat2  30336  paddatclN  30431  osumcllem4N  30441  osumcllem7N  30444  ltrncoval  30627  cdleme0aa  30692  cdleme0b  30694  cdleme8  30732  cdlemesner  30778  cdleme22eALTN  30827  cdleme26eALTN  30843  cdleme35h  30938  cdleme50trn2  31033  cdleme  31042  tgrpov  31230  tendotp  31243  tendoidcl  31251  tendo0co2  31270  cdlemkvcl  31324  dvhopvadd  31576  dvhopellsm  31600  dihmeetlem1N  31773  dihmeetlem9N  31798  dihatexv  31821  lcfl7lem  31982  mapdrvallem2  32128  mapdh9a  32273  hdmapevec  32321
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