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

Theorem 3ad2ant3 978
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 452 . 2  |-  ( ( th  /\  ph )  ->  ch )
323adant1 973 1  |-  ( ( ps  /\  th  /\  ph )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934
This theorem is referenced by:  simp3l  983  simp3r  984  simp31  991  simp32  992  simp33  993  simp3ll  1026  simp3lr  1027  simp3rl  1028  simp3rr  1029  simp3l1  1060  simp3l2  1061  simp3l3  1062  simp3r1  1063  simp3r2  1064  simp3r3  1065  simp31l  1078  simp31r  1079  simp32l  1080  simp32r  1081  simp33l  1082  simp33r  1083  simp311  1102  simp312  1103  simp313  1104  simp321  1105  simp322  1106  simp323  1107  simp331  1108  simp332  1109  simp333  1110  3anim123i  1137  3jaao  1249  ceqsalt  2810  ceqsralt  2811  vtoclgft  2834  epne3  4572  limsuc  4640  poltletr  5078  funprg  5301  fsnunf  5718  fsnunfv  5720  fnsuppres  5732  weniso  5852  smoel  6377  smoord  6382  omwordi  6569  oneo  6579  oeord  6586  oewordi  6589  nnmwordi  6633  nnneo  6649  undifixp  6852  domss2  7020  domssex2  7021  unxpdomlem3  7069  dif1enOLD  7090  dif1en  7091  dffi2  7176  unwdomg  7298  ixpiunwdom  7305  oemapvali  7386  en3lplem1  7416  fodomfi2  7687  infcdaabs  7832  infunabs  7833  infdif  7835  ackbij1lem9  7854  ackbij1lem16  7861  coflim  7887  cfsmolem  7896  isfin2-2  7945  fin1a2lem9  8034  hsmexlem2  8053  axcc2lem  8062  axcc3  8064  domtriomlem  8068  axdc3lem4  8079  axcclem  8083  zornn0g  8132  axacndlem4  8232  axacndlem5  8233  axacnd  8234  gchdomtri  8251  fpwwe  8268  tskssel  8379  tskint  8407  tskurn  8411  gruurn  8420  gruixp  8431  grudomon  8439  gruina  8440  adderpqlem  8578  mulerpqlem  8579  addassnq  8582  mulassnq  8583  distrnq  8585  ltsonq  8593  ltanq  8595  ltmnq  8596  reclem3pr  8673  addid2  8995  addcan2  8997  divdir  9447  divcan5  9462  ltdiv1  9620  infmrcl  9733  infmrlb  9735  lt2halves  9946  zdivmul  10084  xaddass  10569  xleadd1  10575  xltadd1  10576  xmulasslem3  10606  xmulass  10607  xlemul1  10610  xlemul2  10611  xltmul1  10612  xadddir  10616  elioo5  10708  iccsupr  10736  iccneg  10757  icoshft  10758  icoshftf1o  10759  iccsplit  10768  fzen  10811  fzrevral  10866  fzshftral  10869  elfzo  10877  modabs  10997  modcyc  10999  moddi  11007  modsubdir  11008  expdiv  11152  leexp2a  11157  bcval3  11319  hashgadd  11359  hashfun  11389  ccatval1  11431  ccatval2  11432  ccatval3  11433  ccatass  11436  swrdval2  11453  splval  11466  ccatco  11490  swrds2  11560  sqr0  11727  elicc4abs  11803  mulcn2  12069  demoivreALT  12481  rpnnen2lem4  12496  dvdsval2  12534  dvdsexp  12584  mulgcd  12725  mulgcdr  12727  gcddiv  12728  rpmulgcd  12734  rplpwr  12735  prmexpb  12796  rpexp  12799  coprimeprodsq  12862  pythagtriplem1  12869  pythagtriplem3  12871  pythagtriplem10  12873  pythagtriplem6  12874  pythagtriplem11  12878  pythagtriplem12  12879  pythagtriplem13  12880  pythagtriplem15  12882  pythagtriplem17  12884  pythagtriplem19  12886  pcdvdsb  12921  pcfaclem  12946  vdwapun  13021  ramval  13055  0ram2  13068  0ramcl  13070  imasaddvallem  13431  imasvscaval  13440  mreiincl  13498  mremre  13506  mrieqv2d  13541  cofurid  13765  xpcpropd  13982  clatleglb  14230  gsumccat  14464  mulgdirlem  14591  mulgp1  14593  eqglact  14668  mndodcongi  14858  oddvdsnn0  14859  odngen  14888  gexnnod  14899  lsmlub  14974  lsmass  14979  efgsval2  15042  efgsrel  15043  ghmplusg  15138  odadd1  15140  odadd2  15141  gsumsn  15220  dvrcan1  15473  dvrcan3  15474  irredrmul  15489  srngadd  15622  srngmul  15623  lmhmvsca  15802  reslmhm2  15810  lbspss  15835  lsmsp  15839  lspsneu  15876  lidldvgen  16007  psropprmul  16316  coe1add  16341  coe1addfv  16342  coe1subfv  16343  coe1tm  16349  coe1sclmul  16358  coe1sclmul2  16360  cssmre  16593  iuncld  16782  clsss  16791  ntrcls0  16813  iscldtop  16832  neiss  16846  neips  16850  restcldi  16904  cnpnei  16993  cnconst2  17011  cnpresti  17016  sslm  17027  cnt0  17074  cnt1  17078  cnhaus  17082  cncmp  17119  cmpcld  17129  cnconn  17148  concompss  17159  elptr  17268  upxp  17317  qtoptop2  17390  ordthmeolem  17492  opnfbas  17537  isfil2  17551  fbasweak  17560  snfbas  17561  fgss  17568  fgcl  17573  fbasrn  17579  trnei  17587  cfinfil  17588  csdfil  17589  supfil  17590  filufint  17615  fin1aufil  17627  fmval  17638  fmf  17640  elfm  17642  elfm3  17645  imaelfm  17646  rnelfmlem  17647  rnelfm  17648  flimclslem  17679  flfneii  17687  cnpfcfi  17735  alexsubALT  17745  ptcmplem3  17748  prdsxmetlem  17932  txmetcn  18094  nmmtri  18143  nmrtri  18145  unitnmn0  18179  nminvr  18180  nmotri  18248  nghmplusg  18249  isclmi  18575  fmcfil  18698  srabn  18777  itgconst  19173  dvn2bss  19279  evlsval  19403  evlsval2  19404  deg1mul3  19501  deg1mul3le  19502  deg1tmle  19503  q1peqb  19540  r1pcl  19543  r1pdeglt  19544  r1pid  19545  dvdsq1p  19546  dvdsr1p  19547  ptolemy  19864  sincosq1eq  19880  cxplt2  20045  pythag  20115  bcmono  20516  efexple  20520  lgsdirnn0  20578  selberglem3  20696  gxpval  20926  gxnval  20927  gxnn0neg  20930  gxnn0suc  20931  gxneg  20933  gxsuc  20939  gxnn0add  20941  gxadd  20942  gxsub  20943  gxnn0mul  20944  gxmul  20945  gxmodid  20946  gxdi  20963  vcid  21107  vcdi  21108  vcdir  21109  vcass  21110  imsmetlem  21259  0oval  21366  ajval  21440  shlub  21993  hmopco  22603  adjlnop  22666  mdslmd4i  22913  ballotlemieq  23075  ballotlemrv1  23079  logeq0im1  23396  sigaclcuni  23479  measxun  23539  measvuni  23542  ind1  23602  ind0  23603  erdszelem2  23723  cnpcon  23761  cvmscld  23804  ghomf1olem  24001  dedekind  24082  dvdspw  24103  dfon2lem3  24141  dfon2lem7  24145  predpo  24184  frrlem4  24284  nofulllem3  24358  brbtwn2  24533  axcgrid  24544  ax5seglem1  24556  ax5seglem2  24557  ax5seg  24566  axpasch  24569  axlowdimlem16  24585  axcontlem7  24598  btwndiff  24650  brcolinear2  24681  btwnconn1  24724  nnssi3  24895  nndivsub  24896  areacirclem4  24927  areacirclem6  24930  areacirc  24931  oprssopvg  25034  uninqs  25039  inttrp  25108  mapmapmap  25148  injsurinj  25149  iscst4  25177  labs1  25188  labs2  25190  isoriso2  25213  int2pre  25237  ubpar  25261  supaub  25273  inposet  25278  toplat  25290  prsubrtr  25399  zerdivemp1  25436  rngoridfz  25437  svli2  25484  npmp  25521  intopcoaconlem3b  25538  conttnf2  25562  cmptdst  25568  limptlimpr2lem2  25575  flfnei2  25577  islimrs  25580  islimrs3  25581  nolimf2  25620  lvsovso  25626  supnufb  25630  claddrv  25647  claddrvr  25648  addassv  25656  addcanri  25666  negveud  25668  negveudr  25669  issubrv  25672  mulmulvec  25687  distsava  25689  divclcvd  25694  divclrvd  25695  icccon4  25702  cmppfd  25745  1cat  25759  imonclem  25813  ismonc  25814  iepiclem  25823  isepic  25824  vtarsu  25886  vtarl  25887  tartarmap  25888  cmp2morpcats  25961  cmppar3  25974  isconc3  26008  pgapspf2  26053  isconcl5ab  26102  isibg1a6  26125  segline  26141  pxysxy  26142  lppotos  26144  bsstrs  26146  nbssntrs  26147  bosser  26167  pdiveql  26168  isibcg  26191  nn0prpwlem  26238  hmeoclda  26251  hmeocldb  26252  ivthALT  26258  ssref  26283  fnemeet1  26315  fnejoin1  26317  upixp  26403  filbcmb  26432  cnresima  26484  smprngopr  26677  igenval2  26691  ismrcd1  26773  istopclsd  26775  ismrc  26776  mapfzcons  26793  eldioph2  26841  diophrex  26855  diophren  26896  pellexlem1  26914  pellexlem5  26918  pellqrexplicit  26962  reglogmul  26978  reglogexp  26979  rmxycomplete  27002  congmul  27054  congabseq  27061  acongsym  27063  acongneg2  27064  fzneg  27069  acongeq  27070  jm2.19  27086  jm2.22  27088  jm2.23  27089  jm2.20nn  27090  rmydioph  27107  rmxdiophlem  27108  jm3.1  27113  pwssplit3  27190  pwssplit4  27191  frlmup4  27253  enfixsn  27257  mapfien2  27258  islindf2  27284  lindsind2  27289  f1lindf  27292  lindsss  27294  f1linds  27295  lindsmm  27298  lbslcic  27311  hbtlem2  27328  mndvcl  27446  mndvass  27447  mhmvlin  27452  idomrootle  27511  dvconstbi  27551  expgrowth  27552  fmul01lt1lem1  27714  climsuselem1  27733  climsuse  27734  stoweidlem3  27752  stoweidlem16  27765  stoweidlem17  27766  stoweidlem26  27775  stoweidlem34  27783  stoweidlem57  27806  f1oun2prg  28076  nbusgra  28143  cusgra2v  28158  3vfriswmgralem  28182  3vfriswmgra  28183  chordthmALT  28710  bnj837  28791  bnj517  28917  bnj553  28930  bnj594  28944  bnj967  28977  bnj1097  29011  bnj1110  29012  bnj1118  29014  bnj1128  29020  bnj1125  29022  bnj1145  29023  bnj1136  29027  bnj1173  29032  bnj1189  29039  bnj1204  29042  bnj1279  29048  bnj1321  29057  bnj1413  29065  lsmsat  29198  lsmsatcv  29200  lsatcvatlem  29239  islshpcv  29243  l1cvpat  29244  lfli  29251  lshpset2N  29309  cvrnbtwn  29461  meetat2  29487  atcmp  29501  atcvreq0  29504  atlatmstc  29509  cvlcvr1  29529  cvlcvrp  29530  cvlatcvr2  29532  cvr2N  29600  cvratlem  29610  2atjm  29634  athgt  29645  2lplnmN  29748  2llnmj  29749  2lplnmj  29811  dalemswapyzps  29879  dalem23  29885  dalem24  29886  dalem25  29887  dalem27  29888  dalem28  29889  dalem38  29899  dalem39  29900  dalem44  29905  dalem45  29906  dalem51  29912  dalem52  29913  dalem56  29917  pmapglbx  29958  pmapjat1  30042  pmapjat2  30043  paddatclN  30138  osumcllem4N  30148  osumcllem7N  30151  ltrncoval  30334  cdleme0aa  30399  cdleme0b  30401  cdleme8  30439  cdlemesner  30485  cdleme22eALTN  30534  cdleme26eALTN  30550  cdleme35h  30645  cdleme50trn2  30740  cdleme  30749  tgrpov  30937  tendotp  30950  tendoidcl  30958  tendo0co2  30977  cdlemkvcl  31031  dvhopvadd  31283  dvhopellsm  31307  dihmeetlem1N  31480  dihmeetlem9N  31505  dihatexv  31528  lcfl7lem  31689  mapdrvallem2  31835  mapdh9a  31980  hdmapevec  32028
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator