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  2923  ceqsralt  2924  vtoclgft  2947  prnebg  3923  epne3  4703  limsuc  4771  poltletr  5211  funprg  5442  funtpg  5443  fntpg  5448  ftpg  5857  fsnunf  5872  fsnunfv  5874  fvpr1g  5878  fvpr2g  5879  fnsuppres  5893  weniso  6016  smoel  6560  smoord  6565  omwordi  6752  oneo  6762  oeord  6769  oewordi  6772  nnmwordi  6816  nnneo  6832  uniinqs  6922  undifixp  7036  domss2  7204  domssex2  7205  unxpdomlem3  7253  dif1enOLD  7278  dif1en  7279  dffi2  7365  unwdomg  7487  ixpiunwdom  7494  oemapvali  7575  en3lplem1  7605  fodomfi2  7876  infcdaabs  8021  infunabs  8022  infdif  8024  ackbij1lem9  8043  ackbij1lem16  8050  coflim  8076  cfsmolem  8085  isfin2-2  8134  fin1a2lem9  8223  hsmexlem2  8242  axcc2lem  8251  axcc3  8253  domtriomlem  8257  axdc3lem4  8268  axcclem  8272  zornn0g  8320  axacndlem4  8420  axacndlem5  8421  axacnd  8422  gchdomtri  8439  fpwwe  8456  tskssel  8567  tskint  8595  tskurn  8599  gruurn  8608  gruixp  8619  grudomon  8627  gruina  8628  adderpqlem  8766  mulerpqlem  8767  addassnq  8770  mulassnq  8771  distrnq  8773  ltsonq  8781  ltanq  8783  ltmnq  8784  reclem3pr  8861  addid2  9183  addcan2  9185  divdir  9635  divcan5  9650  ltdiv1  9808  infmrcl  9921  infmrlb  9923  lt2halves  10136  zdivmul  10276  xaddass  10762  xleadd1  10768  xltadd1  10769  xmulasslem3  10799  xmulass  10800  xlemul1  10803  xlemul2  10804  xltmul1  10805  xadddir  10809  elioo5  10902  iccsupr  10931  iccneg  10952  icoshft  10953  icoshftf1o  10954  iccsplit  10963  fzen  11006  fzrevral  11063  fzshftral  11066  elfzo  11074  modabs  11203  modcyc  11205  moddi  11213  modsubdir  11214  expdiv  11359  leexp2a  11364  bcval3  11526  hashnnn0genn0  11556  hashgadd  11580  hashunx  11589  hashtpg  11620  hashfun  11629  brfi1indlem  11643  ccatval1  11674  ccatval2  11675  ccatval3  11676  ccatass  11679  swrdval2  11696  splval  11709  ccatco  11733  f1oun2prg  11793  swrds2  11809  sqr0  11976  elicc4abs  12052  mulcn2  12318  demoivreALT  12731  rpnnen2lem4  12746  dvdsval2  12784  dvdsexp  12834  mulgcd  12975  mulgcdr  12977  gcddiv  12978  rpmulgcd  12984  rplpwr  12985  prmexpb  13046  rpexp  13049  coprimeprodsq  13112  pythagtriplem1  13119  pythagtriplem3  13121  pythagtriplem10  13123  pythagtriplem6  13124  pythagtriplem11  13128  pythagtriplem12  13129  pythagtriplem13  13130  pythagtriplem15  13132  pythagtriplem17  13134  pythagtriplem19  13136  pcdvdsb  13171  pcfaclem  13196  vdwapun  13271  ramval  13305  0ram2  13318  0ramcl  13320  imasaddvallem  13683  imasvscaval  13692  mreiincl  13750  mremre  13758  mrieqv2d  13793  cofurid  14017  xpcpropd  14234  clatleglb  14482  gsumccat  14716  mulgdirlem  14843  mulgp1  14845  eqglact  14920  mndodcongi  15110  oddvdsnn0  15111  odngen  15140  gexnnod  15151  lsmlub  15226  lsmass  15231  efgsval2  15294  efgsrel  15295  ghmplusg  15390  odadd1  15392  odadd2  15393  gsumsn  15472  dvrcan1  15725  dvrcan3  15726  irredrmul  15741  srngadd  15874  srngmul  15875  lmhmvsca  16050  reslmhm2  16058  lbspss  16083  lsmsp  16087  lspsneu  16124  lidldvgen  16255  psropprmul  16561  coe1add  16586  coe1addfv  16587  coe1subfv  16588  coe1tm  16594  coe1sclmul  16603  coe1sclmul2  16605  cssmre  16845  iuncld  17034  clsss  17043  ntrcls0  17065  iscldtop  17084  neiss  17098  neips  17102  restcldi  17161  cnpnei  17252  cnconst2  17271  cnpresti  17276  sslm  17287  cnt0  17334  cnt1  17338  cnhaus  17342  cncmp  17379  cmpcld  17389  cnconn  17408  concompss  17419  elptr  17528  upxp  17578  qtoptop2  17654  ordthmeolem  17756  opnfbas  17797  isfil2  17811  fbasweak  17820  snfbas  17821  fgss  17828  fgcl  17833  fbasrn  17839  trnei  17847  cfinfil  17848  csdfil  17849  supfil  17850  filufint  17875  fin1aufil  17887  fmval  17898  fmf  17900  elfm  17902  elfm3  17905  imaelfm  17906  rnelfmlem  17907  rnelfm  17908  flimclslem  17939  flfneii  17947  cnpfcfi  17995  alexsubALT  18005  ptcmplem3  18008  ustref  18171  ustelimasn  18175  utop3cls  18204  ressusp  18218  cfiluexsm  18243  prdsxmetlem  18308  txmetcn  18470  nmmtri  18541  nmrtri  18543  unitnmn0  18577  nminvr  18578  nmotri  18646  nghmplusg  18647  isclmi  18975  fmcfil  19098  srabn  19183  itgconst  19579  dvn2bss  19685  evlsval  19809  evlsval2  19810  deg1mul3  19907  deg1mul3le  19908  deg1tmle  19909  q1peqb  19946  r1pcl  19949  r1pdeglt  19950  r1pid  19951  dvdsq1p  19952  dvdsr1p  19953  ptolemy  20273  sincosq1eq  20289  logmul2  20380  logdiv2  20381  cxplt2  20458  pythag  20528  bcmono  20930  efexple  20934  lgsdirnn0  20992  selberglem3  21110  nbusgra  21308  nbgraf1olem1  21319  nbusgrafi  21326  nb3graprlem1  21328  nb3graprlem2  21329  cusgra2v  21339  cusgra3v  21341  constr1trl  21438  constr2trl  21448  2pthon  21452  constr3lem4  21484  constr3trllem2  21488  constr3trllem5  21491  constr3pthlem2  21493  vdgrfival  21518  vdgrf  21519  vdgrfif  21520  vdusgra0nedg  21529  hashnbgravd  21531  gxpval  21697  gxnval  21698  gxnn0neg  21701  gxnn0suc  21702  gxneg  21704  gxsuc  21710  gxnn0add  21712  gxadd  21713  gxsub  21714  gxnn0mul  21715  gxmul  21716  gxmodid  21717  gxdi  21734  zerdivemp1  21872  rngoridfz  21873  vcid  21880  vcdi  21881  vcdir  21882  vcass  21883  imsmetlem  22032  0oval  22139  ajval  22213  shlub  22766  hmopco  23376  adjlnop  23439  mdslmd4i  23686  divnumden2  24001  ress0g  24023  ressnm  24025  ofldadd  24066  ofldmul  24067  logeq0im1  24192  ind1  24214  ind0  24215  sigaclcuni  24299  sigagenss2  24331  measun  24361  measvuni  24364  dya2iocnrect  24427  ballotlemieq  24555  ballotlemrv1  24559  lgamgulmlem1  24594  erdszelem2  24659  cnpcon  24698  cvmscld  24741  ghomf1olem  24886  dedekind  24968  prodfrec  25004  ntrivcvgfvn0  25008  dvdspw  25129  dfon2lem3  25167  dfon2lem7  25171  predpo  25210  frrlem4  25310  nofulllem3  25384  brbtwn2  25560  axcgrid  25571  ax5seglem1  25583  ax5seglem2  25584  ax5seg  25593  axpasch  25596  axlowdimlem16  25612  axcontlem7  25625  btwndiff  25677  brcolinear2  25708  btwnconn1  25751  nnssi3  25922  nndivsub  25923  areacirclem4  25986  areacirclem6  25989  areacirc  25990  nn0prpwlem  26018  hmeoclda  26029  hmeocldb  26030  ivthALT  26031  ssref  26056  fnemeet1  26088  fnejoin1  26090  upixp  26124  filbcmb  26135  cnresima  26166  smprngopr  26355  igenval2  26369  ismrcd1  26445  istopclsd  26447  ismrc  26448  mapfzcons  26465  eldioph2  26513  diophrex  26527  diophren  26567  pellexlem1  26585  pellexlem5  26589  pellqrexplicit  26633  reglogmul  26649  reglogexp  26650  rmxycomplete  26673  congmul  26725  congabseq  26732  acongsym  26734  acongneg2  26735  fzneg  26740  acongeq  26741  jm2.19  26757  jm2.22  26759  jm2.23  26760  jm2.20nn  26761  rmydioph  26778  rmxdiophlem  26779  jm3.1  26784  pwssplit3  26861  pwssplit4  26862  frlmup4  26924  enfixsn  26928  mapfien2  26929  islindf2  26955  lindsind2  26960  f1lindf  26963  lindsss  26965  f1linds  26966  lindsmm  26969  lbslcic  26982  hbtlem2  26999  mndvcl  27117  mndvass  27118  mhmvlin  27123  idomrootle  27182  dvconstbi  27222  expgrowth  27223  fmul01lt1lem1  27384  climsuselem1  27403  climsuse  27404  stoweidlem3  27422  stoweidlem16  27435  stoweidlem17  27436  stoweidlem26  27445  stoweidlem34  27453  stoweidlem57  27476  3vfriswmgralem  27759  3vfriswmgra  27760  chordthmALT  28389  bnj837  28470  bnj517  28596  bnj553  28609  bnj594  28623  bnj967  28656  bnj1097  28690  bnj1110  28691  bnj1118  28693  bnj1128  28699  bnj1125  28701  bnj1145  28702  bnj1136  28706  bnj1173  28711  bnj1189  28718  bnj1204  28721  bnj1279  28727  bnj1321  28736  bnj1413  28744  lsmsat  29125  lsmsatcv  29127  lsatcvatlem  29166  islshpcv  29170  l1cvpat  29171  lfli  29178  lshpset2N  29236  cvrnbtwn  29388  meetat2  29414  atcmp  29428  atcvreq0  29431  atlatmstc  29436  cvlcvr1  29456  cvlcvrp  29457  cvlatcvr2  29459  cvr2N  29527  cvratlem  29537  2atjm  29561  athgt  29572  2lplnmN  29675  2llnmj  29676  2lplnmj  29738  dalemswapyzps  29806  dalem23  29812  dalem24  29813  dalem25  29814  dalem27  29815  dalem28  29816  dalem38  29826  dalem39  29827  dalem44  29832  dalem45  29833  dalem51  29839  dalem52  29840  dalem56  29844  pmapglbx  29885  pmapjat1  29969  pmapjat2  29970  paddatclN  30065  osumcllem4N  30075  osumcllem7N  30078  ltrncoval  30261  cdleme0aa  30326  cdleme0b  30328  cdleme8  30366  cdlemesner  30412  cdleme22eALTN  30461  cdleme26eALTN  30477  cdleme35h  30572  cdleme50trn2  30667  cdleme  30676  tgrpov  30864  tendotp  30877  tendoidcl  30885  tendo0co2  30904  cdlemkvcl  30958  dvhopvadd  31210  dvhopellsm  31234  dihmeetlem1N  31407  dihmeetlem9N  31432  dihatexv  31455  lcfl7lem  31616  mapdrvallem2  31762  mapdh9a  31907  hdmapevec  31955
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