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

Theorem 3ad2ant3 1020
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 1015 1  |-  ( ( ps  /\  th  /\  ph )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 974
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 976
This theorem is referenced by:  simp3l  1025  simp3r  1026  simp31  1033  simp32  1034  simp33  1035  simp3ll  1068  simp3lr  1069  simp3rl  1070  simp3rr  1071  simp3l1  1102  simp3l2  1103  simp3l3  1104  simp3r1  1105  simp3r2  1106  simp3r3  1107  simp31l  1120  simp31r  1121  simp32l  1122  simp32r  1123  simp33l  1124  simp33r  1125  simp311  1144  simp312  1145  simp313  1146  simp321  1147  simp322  1148  simp323  1149  simp331  1150  simp332  1151  simp333  1152  3anim123i  1182  3jaao  1297  ceqsalt  3118  ceqsralt  3119  vtoclgft  3143  tpssi  4181  prnebg  4197  otthg  4720  poltletr  5392  funprg  5627  funtpg  5628  fntpg  5633  ftpg  6066  fsnunf  6094  fsnunfv  6096  fvpr1g  6101  fvpr2g  6102  fnsuppresOLD  6116  weniso  6235  ovmpt3rab1  6519  epne3  6601  limsuc  6669  oteqimp  6804  el2xptp0  6829  funsssuppss  6928  smoel  7033  smoord  7038  omwordi  7222  oneo  7232  oeord  7239  oewordi  7242  nnmwordi  7286  nnneo  7302  uniinqs  7393  undifixp  7507  enfixsn  7628  domss2  7678  domssex2  7679  unxpdomlem3  7728  dif1enOLD  7754  dif1en  7755  mapfien2  7870  dffi2  7885  unwdomg  8013  ixpiunwdom  8020  en3lplem1  8034  oemapvali  8106  fodomfi2  8444  infcdaabs  8589  infunabs  8590  infdif  8592  ackbij1lem9  8611  ackbij1lem16  8618  coflim  8644  cfsmolem  8653  isfin2-2  8702  fin1a2lem9  8791  hsmexlem2  8810  axcc2lem  8819  axcc3  8821  domtriomlem  8825  axdc3lem4  8836  axcclem  8840  zornn0g  8888  axacndlem4  8991  axacndlem5  8992  axacnd  8993  gchdomtri  9010  fpwwe  9027  tskssel  9138  tskint  9166  tskurn  9170  gruurn  9179  gruixp  9190  grudomon  9198  gruina  9199  adderpqlem  9335  mulerpqlem  9336  addassnq  9339  mulassnq  9340  distrnq  9342  ltsonq  9350  ltanq  9352  ltmnq  9353  reclem3pr  9430  dedekind  9747  addid2  9766  addcan2  9768  divdir  10237  divcan5  10253  ltdiv1  10413  infmrcl  10529  infmrlb  10531  lt2halves  10780  zdivmul  10942  xaddass  11452  xleadd1  11458  xltadd1  11459  xmulasslem3  11489  xmulass  11490  xlemul1  11493  xlemul2  11494  xltmul1  11495  xadddir  11499  elioo5  11593  iccsupr  11628  iccneg  11652  icoshft  11653  icoshftf1o  11654  iccsplit  11664  fzen  11714  elfz1b  11759  fzrevral  11774  fzshftral  11777  elfz0ubfz0  11789  elfz0fzfz0  11790  fz0fzelfz0  11791  fz0fzdiffz0  11794  elfzo  11813  elfzonlteqm1  11873  ltdifltdiv  11948  modabs  12011  modcyc  12013  modaddmulmod  12035  moddi  12036  modsubdir  12037  expdiv  12198  leexp2a  12203  bcval3  12366  hashnnn0genn0  12398  hashgadd  12427  hashunx  12436  hashfun  12477  hashtpg  12505  brfi1indlem  12513  ccatval1  12577  ccatval2  12578  ccatval3  12579  ccatsymb  12582  ccatass  12587  ccats1val2  12613  swrdval2  12629  swrd0len0  12642  swrd0fv  12648  swrdeq  12653  2swrdeqwrdeq  12660  swrdswrdlem  12666  swrdswrd  12667  swrd0swrd  12668  ccats1swrdeq  12676  ccats1swrdeqrex  12686  swrdccatin12lem2  12696  swrdccat3b  12703  swrdccatid  12704  splval  12709  repswswrd  12738  cshwidxmod  12756  cshwidx0mod  12757  cshwleneq  12767  scshwfzeqfzo  12776  ccatco  12783  cshco  12784  swrdco  12785  f1oun2prg  12847  swrds2  12865  elicc4abs  13134  mulcn2  13400  fsumsplitsnun  13552  modfsummods  13589  prodfrec  13686  ntrivcvgfvn0  13690  demoivreALT  13918  rpnnen2lem4  13933  dvdsval2  13971  dvdsexp  14024  mulgcd  14166  mulgcdr  14168  gcddiv  14169  rpmulgcd  14175  rplpwr  14176  prmexpb  14240  rpexp  14243  modprm0  14312  modprmn0modprm0  14314  coprimeprodsq  14315  pythagtriplem1  14322  pythagtriplem3  14324  pythagtriplem10  14326  pythagtriplem6  14327  pythagtriplem11  14331  pythagtriplem12  14332  pythagtriplem13  14333  pythagtriplem15  14335  pythagtriplem17  14337  pythagtriplem19  14339  pcdvdsb  14374  pcfaclem  14399  vdwapun  14474  ramval  14508  0ram2  14521  0ramcl  14523  imasaddvallem  14908  imasvscaval  14917  mreiincl  14975  mremre  14983  mrieqv2d  15018  cofurid  15239  xpcpropd  15456  clatleglb  15735  ress0g  15928  gsumccat  15988  gsumccatsn  15990  sgrp2nmndlem3  16022  sgrp2nmndlem5  16026  mulgdirlem  16145  mulgp1  16147  eqglact  16231  fvcosymgeq  16433  gsmsymgreqlem2  16435  pmtrprfv3  16458  pmtr3ncomlem1  16477  mndodcongi  16546  oddvdsnn0  16547  odngen  16576  gexnnod  16587  lsmlub  16662  lsmass  16667  efgsval2  16730  efgsrel  16731  ghmplusg  16831  odadd1  16833  odadd2  16834  srg1zr  17159  dvrcan1  17319  dvrcan3  17320  irredrmul  17335  srngadd  17485  srngmul  17486  lmhmvsca  17670  reslmhm2  17678  pwssplit3  17686  lbspss  17707  lsmsp  17711  lspsneu  17748  lidldvgen  17882  assa2ass  17950  evlsval  18167  evlsval2  18168  psropprmul  18258  coe1add  18284  coe1addfv  18285  coe1subfv  18286  coe1tm  18293  coe1sclmul  18302  coe1sclmul2  18304  coe1fzgsumdlem  18322  lply1binom  18327  evl1gsumdlem  18371  zrhpsgninv  18599  zrhpsgnevpm  18605  zrhpsgnodpm  18606  psgndiflemB  18614  cssmre  18702  frlmup4  18813  islindf2  18827  lindsind2  18832  f1lindf  18835  lindsss  18837  f1linds  18838  lindsmm  18841  lbslcic  18854  mndvcl  18871  mndvass  18872  mhmvlin  18877  matecl  18905  matvscacell  18916  mamulid  18921  mamurid  18922  mattposm  18939  madetsumid  18941  matepmcl  18942  matepm2cl  18943  mat1dimbas  18952  mavmulsolcl  19031  mulmarep1el  19052  mulmarep1gsum1  19053  mulmarep1gsum2  19054  1marepvsma1  19063  m1detdiag  19077  mdetdiaglem  19078  mdetdiag  19079  mdetunilem7  19098  mdetunilem9  19100  mdetmul  19103  gsummatr01lem3  19137  gsummatr01lem4  19138  gsummatr01  19139  smadiadetglem2  19152  matinv  19157  slesolinv  19160  cramerimplem1  19163  cramerimp  19166  cramerlem1  19167  pmatcoe1fsupp  19180  mat2pmatbas  19205  decpmatmullem  19250  pmatcollpw3lem  19262  chpscmat  19321  iuncld  19524  clsss  19533  ntrcls0  19555  iscldtop  19574  neiss  19588  neips  19592  restcldi  19652  cnpnei  19743  cnconst2  19762  cnpresti  19767  sslm  19778  cnt0  19825  cnt1  19829  cnhaus  19833  cncmp  19870  cmpcld  19880  cnconn  19901  concompss  19912  ssref  19991  elptr  20052  upxp  20102  qtoptop2  20178  ordthmeolem  20280  opnfbas  20321  isfil2  20335  fbasweak  20344  snfbas  20345  fgss  20352  fgcl  20357  fbasrn  20363  trnei  20371  cfinfil  20372  csdfil  20373  supfil  20374  filufint  20399  fin1aufil  20411  fmval  20422  fmf  20424  elfm  20426  elfm3  20429  imaelfm  20430  rnelfmlem  20431  rnelfm  20432  flimclslem  20463  flfneii  20471  cnpfcfi  20519  alexsubALT  20529  ptcmplem3  20532  ustref  20699  ustelimasn  20703  utop3cls  20732  ressusp  20746  cfiluexsm  20771  prdsxmetlem  20849  txmetcn  21029  nmmtri  21119  nmrtri  21121  unitnmn0  21155  nminvr  21156  nmotri  21224  nghmplusg  21225  isclmi  21555  fmcfil  21689  srabn  21778  rrxmvallem  21809  itgconst  22203  dvn2bss  22311  deg1mul3  22494  deg1mul3le  22495  deg1tmle  22496  q1peqb  22533  r1pcl  22536  r1pdeglt  22537  r1pid  22538  dvdsq1p  22539  dvdsr1p  22540  ptolemy  22867  sincosq1eq  22883  logmul2  22979  logdiv2  22980  cxplt2  23057  pythag  23127  bcmono  23530  efexple  23534  lgsdirnn0  23592  selberglem3  23710  brbtwn2  24186  axcgrid  24197  ax5seglem1  24209  ax5seglem2  24210  ax5seg  24219  axpasch  24222  axlowdimlem16  24238  axcontlem7  24251  nbgraf1olem1  24419  nbusgrafi  24426  nb3graprlem1  24429  nb3graprlem2  24430  cusgra2v  24440  cusgra3v  24442  wlkcomp  24503  wlkelwrd  24508  2trllemH  24532  2trllemE  24533  constr1trl  24568  constr2spthlem1  24574  2pthlem2  24576  2wlklem1  24577  2pthon  24582  usgra2adedgwlkonALT  24594  constr3lem4  24625  constr3trllem2  24629  constr3trllem5  24632  constr3pthlem2  24634  wlkiswwlk2  24675  2wlkeq  24685  usg2wlkeq  24686  usg2wlkeq2  24687  wwlknred  24701  wwlknext  24702  wwlknredwwlkn  24704  wwlknfi  24716  wlknfi  24717  wlknwwlknvbij  24718  wwlkextproplem3  24721  clwlkcomp  24741  clwwlkgt0  24749  clwwlknprop  24750  clwwlkn0  24752  clwwlkel  24771  clwwlkf  24772  clwwlkf1  24774  clwwlkfo  24775  clwwlkvbij  24779  clwwlkext2edg  24780  clwwisshclwwlem1  24783  clwwisshclww  24785  clwwnisshclwwn  24787  erclwwlkeqlen  24790  erclwwlkref  24791  eleclclwwlknlem2  24796  erclwwlkneqlen  24802  erclwwlknref  24803  erclwwlknsym  24804  erclwwlkntr  24805  hashecclwwlkn1  24812  usghashecclwwlk  24813  hashclwwlkn  24814  clwwlkndivn  24815  clwlkfclwwlk  24822  clwlkfoclwwlk  24823  clwlkf1clwwlklem  24827  clwlkf1clwwlk  24828  el2wlkonot  24847  el2spthonot  24848  el2spthonot0  24849  el2wlkonotot0  24850  vdgrfival  24875  vdgrf  24876  vdgrfif  24877  vdusgra0nedg  24886  hashnbgravd  24890  nbhashnn0  24892  isrgra  24904  rusgranumwwlkl1  24924  rusgra0edg  24933  rusgranumwlks  24934  3vfriswmgralem  24982  3vfriswmgra  24983  usgn0fidegnn0  25007  2spotdisj  25039  usg2spot2nb  25043  extwwlkfablem1  25052  clwwlkextfrlem1  25054  extwwlkfablem2  25056  numclwwlkun  25057  numclwwlkovf2ex  25064  extwwlkfab  25068  numclwlk1lem2foa  25069  numclwlk1lem2f1  25072  numclwlk1lem2fo  25073  numclwwlk1  25076  numclwwlk2lem1  25080  numclwlk2lem2f  25081  numclwlk2lem2f1o  25083  numclwwlk2  25085  numclwwlk3  25087  numclwwlk4  25088  numclwwlk6  25091  numclwwlk7  25092  numclwwlk8  25093  frgrareg  25095  frgraregord013  25096  gxpval  25239  gxnval  25240  gxnn0neg  25243  gxnn0suc  25244  gxneg  25246  gxsuc  25252  gxnn0add  25254  gxadd  25255  gxsub  25256  gxnn0mul  25257  gxmul  25258  gxmodid  25259  gxdi  25276  zerdivemp1  25414  rngoridfz  25415  vcid  25422  vcdi  25423  vcdir  25424  vcass  25425  imsmetlem  25574  0oval  25681  ajval  25755  shlub  26310  hmopco  26920  adjlnop  26983  mdslmd4i  27230  fcoinvbr  27439  divnumden2  27587  ressnm  27617  ress1r  27757  pstmfval  27853  pl1cn  27915  logeq0im1  27988  ind1  28010  ind0  28011  sigaclcuni  28096  sigagenss2  28128  measun  28160  measvuni  28163  dya2iocnrect  28230  ballotlemieq  28433  ballotlemrv1  28437  sgn3da  28458  lgamgulmlem1  28549  erdszelem2  28614  cnpcon  28653  cvmscld  28696  mrsubcv  28848  mrsubvr  28849  ghomf1olem  29012  iprodefisumlem  29099  binomrisefac  29140  dvdspw  29151  dfon2lem3  29193  dfon2lem7  29197  predeq123  29221  predpo  29240  frrlem4  29366  nofulllem3  29440  btwndiff  29653  brcolinear2  29684  btwnconn1  29727  nnssi3  29897  nndivsub  29898  ftc1anclem4  30069  areacirclem2  30084  areacirclem5  30087  areacirc  30088  nn0prpwlem  30116  hmeoclda  30127  hmeocldb  30128  ivthALT  30129  fnemeet1  30160  fnejoin1  30162  upixp  30196  filbcmb  30207  cnresima  30236  smprngopr  30425  igenval2  30439  ismrcd1  30606  istopclsd  30608  ismrc  30609  mapfzcons  30624  eldioph2  30671  diophrex  30685  diophren  30723  pellexlem1  30741  pellexlem5  30745  pellqrexplicit  30789  reglogmul  30805  reglogexp  30806  rmxycomplete  30829  congmul  30881  congabseq  30888  acongsym  30890  acongneg2  30891  fzneg  30896  acongeq  30897  jm2.19  30911  jm2.22  30913  jm2.23  30914  jm2.20nn  30915  rmydioph  30932  rmxdiophlem  30933  jm3.1  30938  pwssplit4  31011  mapfien2OLD  31018  hbtlem2  31049  idomrootle  31128  dvconstbi  31215  expgrowth  31216  fmul01lt1lem1  31532  climsuselem1  31567  climsuse  31568  limcperiod  31588  lptre2pt  31600  cncfshift  31630  cncfperiod  31635  icccncfext  31644  dvnmptconst  31692  dvnprodlem1  31697  dvnprodlem2  31698  iblspltprt  31726  itgspltprt  31732  stoweidlem3  31739  stoweidlem16  31752  stoweidlem17  31753  stoweidlem26  31762  stoweidlem34  31770  stoweidlem57  31793  fourierdlem41  31884  fourierdlem42  31885  fourierdlem52  31895  fourierdlem54  31897  fourierdlem74  31917  fourierdlem75  31918  fourierdlem80  31923  fourierdlem94  31937  fourierdlem102  31945  fourierdlem114  31957  etransclem18  31989  etransclem29  32000  etransclem46  32017  elpwdifsn  32250  2leaddle2  32274  ssfz12  32284  fsumsplitsndif  32300  fsummmodsndifre  32301  fsummmodsnunz  32302  usgra2pth  32308  usgvincvad  32358  usgvincvadALT  32361  funcestrcsetclem6  32617  funcestrcsetclem9  32620  funcsetcestrclem6  32632  funcsetcestrclem9  32635  rngccatidOLD  32672  funcringcsetcOLD2lem6  32721  funcringcsetcOLD2lem9  32724  ringccatidOLD  32732  funcringcsetclem6OLD  32744  ofaddmndmap  32801  mapprop  32803  nn0sumltlt  32807  gsumpr  32818  domnmsuppn0  32832  scmsuppss  32835  mndpsuppfi  32838  gsumlsscl  32846  ply1ass23l  32852  ply1mulgsumlem1  32856  lincfsuppcl  32884  linccl  32885  lincvalsng  32887  lincvalpr  32889  lincdifsn  32895  ellcoellss  32906  lincext1  32925  lincext2  32926  lincext3  32927  lindslinindimp2lem2  32930  ldepspr  32944  lincresunit3lem1  32950  lincresunit3lem2  32951  islindeps2  32954  chordthmALT  33601  bnj837  33687  bnj517  33811  bnj553  33824  bnj594  33838  bnj967  33871  bnj1097  33905  bnj1110  33906  bnj1118  33908  bnj1128  33914  bnj1125  33916  bnj1145  33917  bnj1136  33921  bnj1173  33926  bnj1189  33933  bnj1204  33936  bnj1279  33942  bnj1321  33951  bnj1413  33959  bj-ceqsalt1  34333  lsmsat  34608  lsmsatcv  34610  lsatcvatlem  34649  islshpcv  34653  l1cvpat  34654  lfli  34661  lshpset2N  34719  cvrnbtwn  34871  meetat2  34897  atcmp  34911  atcvreq0  34914  atlatmstc  34919  cvlcvr1  34939  cvlcvrp  34940  cvlatcvr2  34942  cvr2N  35010  cvratlem  35020  2atjm  35044  athgt  35055  2lplnmN  35158  2llnmj  35159  2lplnmj  35221  dalemswapyzps  35289  dalem23  35295  dalem24  35296  dalem25  35297  dalem27  35298  dalem28  35299  dalem38  35309  dalem39  35310  dalem44  35315  dalem45  35316  dalem51  35322  dalem52  35323  dalem56  35327  pmapglbx  35368  pmapjat1  35452  pmapjat2  35453  paddatclN  35548  osumcllem4N  35558  osumcllem7N  35561  ltrncoval  35744  cdleme0aa  35810  cdleme0b  35812  cdleme8  35850  cdlemesner  35896  cdleme22eALTN  35946  cdleme26eALTN  35962  cdleme35h  36057  cdleme50trn2  36152  cdleme  36161  tgrpov  36349  tendotp  36362  tendoidcl  36370  tendo0co2  36389  cdlemkvcl  36443  dvhopvadd  36695  dvhopellsm  36719  dihmeetlem1N  36892  dihmeetlem9N  36917  dihatexv  36940  lcfl7lem  37101  mapdrvallem2  37247  mapdh9a  37392  hdmapevec  37440  pwinfi2  37585
  Copyright terms: Public domain W3C validator