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

Theorem 3ad2ant3 1011
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 466 . 2  |-  ( ( th  /\  ph )  ->  ch )
323adant1 1006 1  |-  ( ( ps  /\  th  /\  ph )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 965
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 967
This theorem is referenced by:  simp3l  1016  simp3r  1017  simp31  1024  simp32  1025  simp33  1026  simp3ll  1059  simp3lr  1060  simp3rl  1061  simp3rr  1062  simp3l1  1093  simp3l2  1094  simp3l3  1095  simp3r1  1096  simp3r2  1097  simp3r3  1098  simp31l  1111  simp31r  1112  simp32l  1113  simp32r  1114  simp33l  1115  simp33r  1116  simp311  1135  simp312  1136  simp313  1137  simp321  1138  simp322  1139  simp323  1140  simp331  1141  simp332  1142  simp333  1143  3anim123i  1173  3jaao  1286  ceqsalt  2990  ceqsralt  2991  vtoclgft  3015  tpssi  4034  prnebg  4049  poltletr  5228  funprg  5462  funtpg  5463  fntpg  5468  ftpg  5887  fsnunf  5911  fsnunfv  5913  fvpr1g  5918  fvpr2g  5919  fnsuppresOLD  5933  weniso  6040  epne3  6387  limsuc  6455  funsssuppss  6710  smoel  6813  smoord  6818  omwordi  7002  oneo  7012  oeord  7019  oewordi  7022  nnmwordi  7066  nnneo  7082  uniinqs  7172  undifixp  7291  enfixsn  7412  domss2  7462  domssex2  7463  unxpdomlem3  7511  dif1enOLD  7536  dif1en  7537  mapfien2  7650  dffi2  7665  unwdomg  7791  ixpiunwdom  7798  en3lplem1  7812  oemapvali  7884  fodomfi2  8222  infcdaabs  8367  infunabs  8368  infdif  8370  ackbij1lem9  8389  ackbij1lem16  8396  coflim  8422  cfsmolem  8431  isfin2-2  8480  fin1a2lem9  8569  hsmexlem2  8588  axcc2lem  8597  axcc3  8599  domtriomlem  8603  axdc3lem4  8614  axcclem  8618  zornn0g  8666  axacndlem4  8769  axacndlem5  8770  axacnd  8771  gchdomtri  8788  fpwwe  8805  tskssel  8916  tskint  8944  tskurn  8948  gruurn  8957  gruixp  8968  grudomon  8976  gruina  8977  adderpqlem  9115  mulerpqlem  9116  addassnq  9119  mulassnq  9120  distrnq  9122  ltsonq  9130  ltanq  9132  ltmnq  9133  reclem3pr  9210  dedekind  9525  addid2  9544  addcan2  9546  divdir  10009  divcan5  10025  ltdiv1  10185  infmrcl  10301  infmrlb  10303  lt2halves  10551  zdivmul  10706  xaddass  11204  xleadd1  11210  xltadd1  11211  xmulasslem3  11241  xmulass  11242  xlemul1  11245  xlemul2  11246  xltmul1  11247  xadddir  11251  elioo5  11345  iccsupr  11374  iccneg  11398  icoshft  11399  icoshftf1o  11400  iccsplit  11410  fzen  11459  elfzelfzelfz  11476  elfz0fzfz0  11477  fz0fzelfz0  11478  fz0fzdiffz0  11481  elfz1b  11519  fzrevral  11536  fzshftral  11539  elfzo  11547  ltdifltdiv  11670  modabs  11733  modcyc  11735  modaddmulmod  11757  moddi  11758  modsubdir  11759  expdiv  11906  leexp2a  11911  bcval3  12074  hashnnn0genn0  12106  hashgadd  12132  hashunx  12141  hashtpg  12178  hashfun  12191  brfi1indlem  12210  ccatval1  12268  ccatval2  12269  ccatval3  12270  ccatsymb  12273  ccatass  12278  ccats1val2  12299  swrdval2  12308  swrd0len0  12321  swrd0fv  12327  swrdeq  12332  2swrdeqwrdeq  12339  swrdswrdlem  12345  swrdswrd  12346  swrd0swrd  12347  ccats1swrdeq  12355  swrdccatin12lem2  12372  swrdccat3b  12379  swrdccatid  12380  splval  12385  repswswrd  12414  cshwidxmod  12432  cshwidx0mod  12433  cshwleneq  12443  ccatco  12455  cshco  12456  swrdco  12457  f1oun2prg  12519  swrds2  12537  elicc4abs  12799  mulcn2  13065  demoivreALT  13477  rpnnen2lem4  13492  dvdsval2  13530  dvdsexp  13581  mulgcd  13722  mulgcdr  13724  gcddiv  13725  rpmulgcd  13731  rplpwr  13732  prmexpb  13795  rpexp  13798  modprm0  13865  modprmn0modprm0  13867  coprimeprodsq  13868  pythagtriplem1  13875  pythagtriplem3  13877  pythagtriplem10  13879  pythagtriplem6  13880  pythagtriplem11  13884  pythagtriplem12  13885  pythagtriplem13  13886  pythagtriplem15  13888  pythagtriplem17  13890  pythagtriplem19  13892  pcdvdsb  13927  pcfaclem  13952  vdwapun  14027  ramval  14061  0ram2  14074  0ramcl  14076  imasaddvallem  14459  imasvscaval  14468  mreiincl  14526  mremre  14534  mrieqv2d  14569  cofurid  14793  xpcpropd  15010  clatleglb  15288  ress0g  15442  gsumccat  15510  gsumccatsn  15512  mulgdirlem  15642  mulgp1  15644  eqglact  15723  fvcosymgeq  15925  gsmsymgreqlem2  15927  pmtrprfv3  15951  pmtr3ncomlem1  15970  mndodcongi  16037  oddvdsnn0  16038  odngen  16067  gexnnod  16078  lsmlub  16153  lsmass  16158  efgsval2  16221  efgsrel  16222  ghmplusg  16319  odadd1  16321  odadd2  16322  gsumsn  16439  dvrcan1  16771  dvrcan3  16772  irredrmul  16787  srngadd  16920  srngmul  16921  lmhmvsca  17103  reslmhm2  17111  pwssplit3  17119  lbspss  17140  lsmsp  17144  lspsneu  17181  lidldvgen  17314  evlsval  17580  evlsval2  17581  psropprmul  17668  coe1add  17693  coe1addfv  17694  coe1subfv  17695  coe1tm  17701  coe1sclmul  17710  coe1sclmul2  17712  evl1gsumdlem  17765  zrhpsgninv  17990  zrhpsgnevpm  17996  zrhpsgnodpm  17997  psgndiflemB  18005  cssmre  18093  frlmup4  18204  islindf2  18218  lindsind2  18223  f1lindf  18226  lindsss  18228  f1linds  18229  lindsmm  18232  lbslcic  18245  mndvcl  18266  mndvass  18267  mhmvlin  18272  mamulid  18279  mamurid  18280  matecl  18301  mattposm  18319  madetsumid  18321  matepmcl  18322  matepm2cl  18323  mavmulsolcl  18337  mulmarep1el  18358  mulmarep1gsum1  18359  mulmarep1gsum2  18360  1marepvsma1  18369  mdetunilem7  18399  mdetunilem9  18401  mdetmul  18404  gsummatr01lem3  18438  gsummatr01lem4  18439  gsummatr01  18440  smadiadetglem2  18453  matinv  18458  slesolinv  18461  cramerimplem1  18464  cramerimp  18467  cramerlem1  18468  iuncld  18624  clsss  18633  ntrcls0  18655  iscldtop  18674  neiss  18688  neips  18692  restcldi  18752  cnpnei  18843  cnconst2  18862  cnpresti  18867  sslm  18878  cnt0  18925  cnt1  18929  cnhaus  18933  cncmp  18970  cmpcld  18980  cnconn  19001  concompss  19012  elptr  19121  upxp  19171  qtoptop2  19247  ordthmeolem  19349  opnfbas  19390  isfil2  19404  fbasweak  19413  snfbas  19414  fgss  19421  fgcl  19426  fbasrn  19432  trnei  19440  cfinfil  19441  csdfil  19442  supfil  19443  filufint  19468  fin1aufil  19480  fmval  19491  fmf  19493  elfm  19495  elfm3  19498  imaelfm  19499  rnelfmlem  19500  rnelfm  19501  flimclslem  19532  flfneii  19540  cnpfcfi  19588  alexsubALT  19598  ptcmplem3  19601  ustref  19768  ustelimasn  19772  utop3cls  19801  ressusp  19815  cfiluexsm  19840  prdsxmetlem  19918  txmetcn  20098  nmmtri  20188  nmrtri  20190  unitnmn0  20224  nminvr  20225  nmotri  20293  nghmplusg  20294  isclmi  20624  fmcfil  20758  srabn  20847  rrxmvallem  20878  itgconst  21271  dvn2bss  21379  deg1mul3  21562  deg1mul3le  21563  deg1tmle  21564  q1peqb  21601  r1pcl  21604  r1pdeglt  21605  r1pid  21606  dvdsq1p  21607  dvdsr1p  21608  ptolemy  21933  sincosq1eq  21949  logmul2  22040  logdiv2  22041  cxplt2  22118  pythag  22188  bcmono  22591  efexple  22595  lgsdirnn0  22653  selberglem3  22771  brbtwn2  23102  axcgrid  23113  ax5seglem1  23125  ax5seglem2  23126  ax5seg  23135  axpasch  23138  axlowdimlem16  23154  axcontlem7  23167  nbgraf1olem1  23301  nbusgrafi  23308  nb3graprlem1  23310  nb3graprlem2  23311  cusgra2v  23321  cusgra3v  23323  2trllemH  23402  2trllemE  23403  constr1trl  23438  constr2spthlem1  23444  2pthlem2  23446  2wlklem1  23447  2pthon  23452  constr3lem4  23484  constr3trllem2  23488  constr3trllem5  23491  constr3pthlem2  23493  vdgrfival  23518  vdgrf  23519  vdgrfif  23520  vdusgra0nedg  23529  hashnbgravd  23531  gxpval  23697  gxnval  23698  gxnn0neg  23701  gxnn0suc  23702  gxneg  23704  gxsuc  23710  gxnn0add  23712  gxadd  23713  gxsub  23714  gxnn0mul  23715  gxmul  23716  gxmodid  23717  gxdi  23734  zerdivemp1  23872  rngoridfz  23873  vcid  23880  vcdi  23881  vcdir  23882  vcass  23883  imsmetlem  24032  0oval  24139  ajval  24213  shlub  24768  hmopco  25378  adjlnop  25441  mdslmd4i  25688  divnumden2  26038  ressnm  26063  gsumsnf  26195  ress1r  26208  pstmfval  26275  pl1cn  26337  logeq0im1  26405  ind1  26427  ind0  26428  sigaclcuni  26513  sigagenss2  26545  measun  26577  measvuni  26580  dya2iocnrect  26648  ballotlemieq  26851  ballotlemrv1  26855  sgn3da  26876  lgamgulmlem1  26967  erdszelem2  27032  cnpcon  27071  cvmscld  27114  ghomf1olem  27264  prodfrec  27361  ntrivcvgfvn0  27365  iprodefisumlem  27455  binomrisefac  27496  dvdspw  27507  dfon2lem3  27549  dfon2lem7  27553  predeq123  27577  predpo  27596  frrlem4  27722  nofulllem3  27796  btwndiff  28009  brcolinear2  28040  btwnconn1  28083  nnssi3  28254  nndivsub  28255  ftc1anclem4  28423  areacirclem2  28438  areacirclem5  28441  areacirc  28442  nn0prpwlem  28470  hmeoclda  28481  hmeocldb  28482  ivthALT  28483  ssref  28508  fnemeet1  28540  fnejoin1  28542  upixp  28576  filbcmb  28587  cnresima  28616  smprngopr  28805  igenval2  28819  ismrcd1  28987  istopclsd  28989  ismrc  28990  mapfzcons  29005  eldioph2  29053  diophrex  29067  diophren  29105  pellexlem1  29123  pellexlem5  29127  pellqrexplicit  29171  reglogmul  29187  reglogexp  29188  rmxycomplete  29211  congmul  29263  congabseq  29270  acongsym  29272  acongneg2  29273  fzneg  29278  acongeq  29279  jm2.19  29295  jm2.22  29297  jm2.23  29298  jm2.20nn  29299  rmydioph  29316  rmxdiophlem  29317  jm3.1  29322  pwssplit4  29395  mapfien2OLD  29402  hbtlem2  29433  idomrootle  29513  dvconstbi  29561  expgrowth  29562  fmul01lt1lem1  29718  climsuselem1  29733  climsuse  29734  stoweidlem3  29751  stoweidlem16  29764  stoweidlem17  29765  stoweidlem26  29774  stoweidlem34  29782  stoweidlem57  29805  el2xptp0  30080  oteqimp  30082  otthg  30083  ovmpt3rab1  30114  2leaddle2  30128  ssfz12  30150  elfzonlteqm1  30178  fsumsplitsndif  30191  fsummmodsndifre  30192  fsumsplitsnun  30195  fsummmodsnunre  30196  modfsummods  30197  ccats1swrdeqrex  30212  wlkelwrd  30233  wlkcomp  30239  2wlkeq  30241  usg2wlkeq  30242  usgra2pth  30254  wlkiswwlk2  30284  usg2wlkeq2  30294  wwlknred  30308  wwlknext  30309  wwlknredwwlkn  30311  wwlknfi  30323  wlknfi  30324  wlknwwlknvbij  30325  el2wlkonot  30341  el2spthonot  30342  el2spthonot0  30343  el2wlkonotot0  30344  clwlkcomp  30379  clwwlkgt0  30387  clwwlknprop  30388  clwwlkn0  30390  clwwlkel  30408  clwwlkf  30409  clwwlkf1  30411  clwwlkfo  30412  clwwlkvbij  30416  clwwlkext2edg  30417  clwwisshclwwlem1  30422  clwwisshclww  30424  clwwnisshclwwn  30426  erclwwlkeqlen  30435  erclwwlkref  30436  eleclclwwlknlem2  30444  scshwfzeqfzo  30445  erclwwlkneqlen  30451  erclwwlknref  30452  erclwwlknsym  30453  erclwwlkntr  30454  hashecclwwlkn1  30461  usghashecclwwlk  30462  hashclwwlkn  30463  clwwlkndivn  30464  clwlkfclwwlk  30470  clwlkfoclwwlk  30471  clwlkf1clwwlklem  30475  clwlkf1clwwlk  30476  nbhashnn0  30485  isrgra  30496  rusgranumwlkl1lem1  30511  wwlkextproplem3  30515  rusgra0edg  30526  rusgranumwlks  30527  3vfriswmgralem  30549  3vfriswmgra  30550  usgn0fidegnn0  30575  2spotdisj  30607  usg2spot2nb  30611  extwwlkfablem1  30620  clwwlkextfrlem1  30622  extwwlkfablem2  30624  numclwwlkun  30625  numclwwlkovf2ex  30632  extwwlkfab  30636  numclwlk1lem2foa  30637  numclwlk1lem2f1  30640  numclwlk1lem2fo  30641  numclwwlk1  30644  numclwwlk2lem1  30648  numclwlk2lem2f  30649  numclwlk2lem2f1o  30651  numclwwlk2  30653  numclwwlk3  30655  numclwwlk4  30656  numclwwlk6  30659  numclwwlk7  30660  numclwwlk8  30661  frgrareg  30663  frgraregord013  30664  ofaddmndmap  30686  mapprop  30688  gsumpr  30709  domnmsuppn0  30733  scmsuppss  30736  mndpsuppfi  30739  gsumlsscl  30753  assa2ass  30758  ply1ass23l  30767  lply1binom  30774  matvscacell  30784  mat1dimbas  30791  pmatcollpw1lem3  30816  pmatcollpw1lem4  30817  pmatcollpw1lem5  30818  pmatcollpw2lem  30820  m1detdiag  30823  mdetdiaglem  30824  mdetdiag  30825  lincfsuppcl  30836  linccl  30837  lincvalsng  30839  lincvalpr  30841  lincdifsn  30847  ellcoellss  30858  lincext1  30877  lincext2  30878  lincext3  30879  lindslinindimp2lem2  30882  ldepspr  30896  lincresunit3lem1  30902  lincresunit3lem2  30903  islindeps2  30906  chordthmALT  31556  bnj837  31641  bnj517  31765  bnj553  31778  bnj594  31792  bnj967  31825  bnj1097  31859  bnj1110  31860  bnj1118  31862  bnj1128  31868  bnj1125  31870  bnj1145  31871  bnj1136  31875  bnj1173  31880  bnj1189  31887  bnj1204  31890  bnj1279  31896  bnj1321  31905  bnj1413  31913  bj-ceqsalt1  32234  lsmsat  32493  lsmsatcv  32495  lsatcvatlem  32534  islshpcv  32538  l1cvpat  32539  lfli  32546  lshpset2N  32604  cvrnbtwn  32756  meetat2  32782  atcmp  32796  atcvreq0  32799  atlatmstc  32804  cvlcvr1  32824  cvlcvrp  32825  cvlatcvr2  32827  cvr2N  32895  cvratlem  32905  2atjm  32929  athgt  32940  2lplnmN  33043  2llnmj  33044  2lplnmj  33106  dalemswapyzps  33174  dalem23  33180  dalem24  33181  dalem25  33182  dalem27  33183  dalem28  33184  dalem38  33194  dalem39  33195  dalem44  33200  dalem45  33201  dalem51  33207  dalem52  33208  dalem56  33212  pmapglbx  33253  pmapjat1  33337  pmapjat2  33338  paddatclN  33433  osumcllem4N  33443  osumcllem7N  33446  ltrncoval  33629  cdleme0aa  33694  cdleme0b  33696  cdleme8  33734  cdlemesner  33780  cdleme22eALTN  33829  cdleme26eALTN  33845  cdleme35h  33940  cdleme50trn2  34035  cdleme  34044  tgrpov  34232  tendotp  34245  tendoidcl  34253  tendo0co2  34272  cdlemkvcl  34326  dvhopvadd  34578  dvhopellsm  34602  dihmeetlem1N  34775  dihmeetlem9N  34800  dihatexv  34823  lcfl7lem  34984  mapdrvallem2  35130  mapdh9a  35275  hdmapevec  35323
  Copyright terms: Public domain W3C validator