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

Theorem 3ad2ant3 1032
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 472 . 2  |-  ( ( th  /\  ph )  ->  ch )
323adant1 1027 1  |-  ( ( ps  /\  th  /\  ph )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 986
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 190  df-an 377  df-3an 988
This theorem is referenced by:  simp3l  1037  simp3r  1038  simp31  1045  simp32  1046  simp33  1047  simp3ll  1080  simp3lr  1081  simp3rl  1082  simp3rr  1083  simp3l1  1114  simp3l2  1115  simp3l3  1116  simp3r1  1117  simp3r2  1118  simp3r3  1119  simp31l  1132  simp31r  1133  simp32l  1134  simp32r  1135  simp33l  1136  simp33r  1137  simp311  1156  simp312  1157  simp313  1158  simp321  1159  simp322  1160  simp323  1161  simp331  1162  simp332  1163  simp333  1164  3anim123i  1194  3jaao  1340  ceqsalt  3038  ceqsralt  3039  vtoclgft  3064  euelss  3698  tpssi  4107  prnebg  4127  otthg  4658  poltletr  5210  predeq123  5360  predpo  5377  funprg  5610  funtpg  5611  fntpg  5616  funcnvpr  5618  funcnvtp  5619  ftpg  6059  fsnunf  6087  fsnunfv  6089  fvpr1g  6094  fvpr2g  6095  weniso  6231  ovmpt3rab1  6513  epne3  6595  limsuc  6664  oteqimp  6800  el2xptp0  6825  funsssuppss  6929  smoel  7066  smoord  7071  omwordi  7259  oneo  7269  oeord  7276  oewordi  7279  nnmwordi  7323  nnneo  7339  uniinqs  7430  undifixp  7545  enfixsn  7668  domss2  7718  domssex2  7719  unxpdomlem3  7765  dif1en  7791  mapfien2  7909  dffi2  7924  unwdomg  8086  ixpiunwdom  8093  en3lplem1  8106  oemapvali  8176  fodomfi2  8478  infcdaabs  8623  infunabs  8624  infdif  8626  ackbij1lem9  8645  ackbij1lem16  8652  coflim  8678  cfsmolem  8687  isfin2-2  8736  fin1a2lem9  8825  hsmexlem2  8844  axcc2lem  8853  axcc3  8855  domtriomlem  8859  axdc3lem4  8870  axcclem  8874  zornn0g  8922  axacndlem4  9022  axacndlem5  9023  axacnd  9024  gchdomtri  9041  fpwwe  9058  tskssel  9169  tskint  9197  tskurn  9201  gruurn  9210  gruixp  9221  grudomon  9229  gruina  9230  adderpqlem  9366  mulerpqlem  9367  addassnq  9370  mulassnq  9371  distrnq  9373  ltsonq  9381  ltanq  9383  ltmnq  9384  reclem3pr  9461  dedekind  9784  addid2  9803  addcan2  9805  divdir  10282  divcan5  10298  ltdiv1  10458  infmrclOLD  10582  infrelb  10585  infmrlbOLD  10586  lt2halves  10837  zdivmul  10998  xaddass  11525  xleadd1  11531  xltadd1  11532  xmulasslem3  11562  xmulass  11563  xlemul1  11566  xlemul2  11567  xltmul1  11568  xadddir  11572  elioo5  11682  iccsupr  11717  iccneg  11744  icoshft  11745  icoshftf1o  11746  iccsplit  11756  fzen  11807  elfz1b  11855  fzrevral  11870  fzshftral  11873  elfz0ubfz0  11886  elfz0fzfz0  11887  fz0fzelfz0  11888  fz0fzdiffz0  11891  elfzo  11915  elfzonlteqm1  11982  ltdifltdiv  12060  modabs  12124  modcyc  12126  modaddmulmod  12150  moddi  12151  modsubdir  12152  expdiv  12317  leexp2a  12322  bcval3  12485  hashnnn0genn0  12520  hashgadd  12550  hashunx  12559  hashfun  12604  hash2prd  12629  hashtpg  12636  brfi1indlem  12644  ccatval1  12720  ccatval2  12721  ccatval3  12722  ccatsymb  12725  ccatass  12730  ccats1val2  12759  swrdval2  12775  swrd0len0  12791  swrd0fv  12794  swrdeq  12799  swrdspsleq  12804  2swrdeqwrdeq  12808  swrdswrdlem  12814  swrdswrd  12815  swrd0swrd  12816  ccats1swrdeq  12824  ccats1swrdeqrex  12834  swrdccatin12lem2  12844  swrdccat3b  12851  swrdccatid  12852  splval  12857  repswswrd  12886  cshwidxmod  12904  cshwidx0mod  12905  cshwleneq  12915  scshwfzeqfzo  12924  ccatco  12931  cshco  12932  swrdco  12933  f1oun2prg  13010  swrds2  13028  trclfvss  13081  elicc4abs  13393  mulcn2  13670  fsumsplitsnun  13827  modfsummods  13864  prodfrec  13962  ntrivcvgfvn0  13966  binomrisefac  14106  demoivreALT  14266  rpnnen2lem4  14281  dvdsval2  14319  dvdsexp  14372  mulgcd  14525  mulgcdr  14527  gcddiv  14528  rpmulgcd  14534  rplpwr  14535  lcmfn0val  14604  lcmfn0valOLD  14607  lcmftp  14620  lcmfunsnlem2lem1  14622  lcmfunsnlem2lem2  14623  lcmfunsnlem2  14624  prmexpb  14681  rpexp  14683  modprm0  14767  modprmn0modprm0  14769  coprimeprodsq  14770  pythagtriplem1  14777  pythagtriplem3  14779  pythagtriplem10  14781  pythagtriplem6  14782  pythagtriplem11  14786  pythagtriplem12  14787  pythagtriplem13  14788  pythagtriplem15  14790  pythagtriplem17  14792  pythagtriplem19  14794  pcdvdsb  14829  pcfaclem  14854  vdwapun  14935  ramval  14971  ramvalOLD  14972  0ram2  14990  0ramcl  14992  fvprmselgcd1  15014  prmgaplem6  15037  imasaddvallem  15446  imasvscaval  15455  mreiincl  15513  mremre  15521  mrieqv2d  15556  cofurid  15807  initoeu2lem0  15919  initoeu2lem2  15921  funcestrcsetclem6  16041  funcestrcsetclem9  16044  funcsetcestrclem6  16056  funcsetcestrclem9  16059  xpcpropd  16104  clatleglb  16383  ress0g  16576  gsumccat  16636  gsumccatsn  16638  sgrp2nmndlem3  16670  sgrp2nmndlem5  16674  mulgdirlem  16793  mulgp1  16795  eqglact  16879  fvcosymgeq  17081  gsmsymgreqlem2  17083  pmtrprfv3  17106  pmtr3ncomlem1  17125  mndodcongi  17203  oddvdsnn0  17204  odngen  17237  gexnnod  17251  lsmlub  17326  lsmass  17331  efgsval2  17394  efgsrel  17395  ghmplusg  17495  odadd1  17497  odadd2  17498  srg1zr  17773  dvrcan1  17930  dvrcan3  17931  irredrmul  17946  srngadd  18096  srngmul  18097  lmhmvsca  18279  reslmhm2  18287  pwssplit3  18295  lbspss  18316  lsmsp  18320  lspsneu  18357  lidldvgen  18490  assa2ass  18557  evlsval  18753  evlsval2  18754  psropprmul  18842  coe1add  18868  coe1addfv  18869  coe1subfv  18870  coe1tm  18877  coe1sclmul  18886  coe1sclmul2  18888  coe1fzgsumdlem  18906  lply1binom  18911  evl1gsumdlem  18955  zrhpsgninv  19164  zrhpsgnevpm  19170  zrhpsgnodpm  19171  psgndiflemB  19179  cssmre  19267  frlmup4  19370  islindf2  19383  lindsind2  19388  f1lindf  19391  lindsss  19393  f1linds  19394  lindsmm  19397  lbslcic  19410  mndvcl  19427  mndvass  19428  mhmvlin  19433  matecl  19461  matvscacell  19472  mamulid  19477  mamurid  19478  mattposm  19495  madetsumid  19497  matepmcl  19498  matepm2cl  19499  mat1dimbas  19508  mavmulsolcl  19587  mulmarep1el  19608  mulmarep1gsum1  19609  mulmarep1gsum2  19610  1marepvsma1  19619  m1detdiag  19633  mdetdiaglem  19634  mdetdiag  19635  mdetunilem7  19654  mdetunilem9  19656  mdetmul  19659  gsummatr01lem3  19693  gsummatr01lem4  19694  gsummatr01  19695  smadiadetglem2  19708  matinv  19713  slesolinv  19716  cramerimplem1  19719  cramerimp  19722  cramerlem1  19723  pmatcoe1fsupp  19736  mat2pmatbas  19761  decpmatmullem  19806  pmatcollpw3lem  19818  chpscmat  19877  iuncld  20071  clsss  20080  ntrcls0  20103  iscldtop  20122  neiss  20136  neips  20140  restcldi  20200  cnpnei  20291  cnconst2  20310  cnpresti  20315  sslm  20326  cnt0  20373  cnt1  20377  cnhaus  20381  cncmp  20418  cmpcld  20428  cnconn  20448  concompss  20459  ssref  20538  elptr  20599  upxp  20649  qtoptop2  20725  ordthmeolem  20827  opnfbas  20868  isfil2  20882  fbasweak  20891  snfbas  20892  fgss  20899  fgcl  20904  fbasrn  20910  trnei  20918  cfinfil  20919  csdfil  20920  supfil  20921  filufint  20946  fin1aufil  20958  fmval  20969  fmf  20971  elfm  20973  elfm3  20976  imaelfm  20977  rnelfmlem  20978  rnelfm  20979  flimclslem  21010  flfneii  21018  cnpfcfi  21066  alexsubALT  21077  ptcmplem3  21080  ustref  21244  ustelimasn  21248  utop3cls  21277  ressusp  21291  cfiluexsm  21316  prdsxmetlem  21394  txmetcn  21574  nmmtri  21646  nmrtri  21648  unitnmn0  21682  nminvr  21683  nmotri  21771  nghmplusg  21772  isclmi  22119  fmcfil  22253  srabn  22338  rrxmvallem  22369  itgconst  22788  dvn2bss  22896  deg1mul3  23076  deg1mul3le  23077  deg1tmle  23078  q1peqb  23117  r1pcl  23120  r1pdeglt  23121  r1pid  23122  dvdsq1p  23123  dvdsr1p  23124  ptolemy  23463  sincosq1eq  23479  logeq0im1  23539  logmul2  23577  logdiv2  23578  cxplt2  23655  logbchbase  23720  relogbreexp  23724  relogbexp  23729  pythag  23758  lgamgulmlem1  23966  bcmono  24217  efexple  24221  lgsdirnn0  24279  selberglem3  24397  brbtwn2  24947  axcgrid  24958  ax5seglem1  24970  ax5seglem2  24971  ax5seg  24980  axpasch  24983  axlowdimlem16  24999  axcontlem7  25012  nbgraf1olem1  25181  nbusgrafi  25188  nb3graprlem1  25191  nb3graprlem2  25192  cusgra2v  25202  cusgra3v  25204  wlkcomp  25265  wlkelwrd  25270  2trllemH  25294  2trllemE  25295  constr1trl  25330  constr2spthlem1  25336  2pthlem2  25338  2wlklem1  25339  2pthon  25344  usgra2adedgwlkonALT  25356  constr3lem4  25387  constr3trllem2  25391  constr3trllem5  25394  constr3pthlem2  25396  wlkiswwlk2  25437  2wlkeq  25447  usg2wlkeq  25448  usg2wlkeq2  25449  wwlknred  25463  wwlknext  25464  wwlknredwwlkn  25466  wwlknfi  25478  wlknfi  25479  wlknwwlknvbij  25480  wwlkextproplem3  25483  clwlkcomp  25503  clwwlkgt0  25511  clwwlknprop  25512  clwwlkn0  25514  clwwlkel  25533  clwwlkf  25534  clwwlkf1  25536  clwwlkfo  25537  clwwlkvbij  25541  clwwlkext2edg  25542  clwwisshclwwlem1  25545  clwwisshclww  25547  clwwnisshclwwn  25549  erclwwlkeqlen  25552  erclwwlkref  25553  eleclclwwlknlem2  25558  erclwwlkneqlen  25564  erclwwlknref  25565  erclwwlknsym  25566  erclwwlkntr  25567  hashecclwwlkn1  25574  usghashecclwwlk  25575  hashclwwlkn  25576  clwwlkndivn  25577  clwlkfclwwlk  25584  clwlkfoclwwlk  25585  clwlkf1clwwlklem  25589  clwlkf1clwwlk  25590  el2wlkonot  25609  el2spthonot  25610  el2spthonot0  25611  el2wlkonotot0  25612  vdgrfival  25637  vdgrf  25638  vdgrfif  25639  vdusgra0nedg  25648  hashnbgravd  25652  nbhashnn0  25654  isrgra  25666  rusgranumwwlkl1  25686  rusgra0edg  25695  rusgranumwlks  25696  3vfriswmgralem  25744  3vfriswmgra  25745  usgn0fidegnn0  25769  2spotdisj  25801  usg2spot2nb  25805  extwwlkfablem1  25814  clwwlkextfrlem1  25816  extwwlkfablem2  25818  numclwwlkun  25819  numclwwlkovf2ex  25826  extwwlkfab  25830  numclwlk1lem2foa  25831  numclwlk1lem2f1  25834  numclwlk1lem2fo  25835  numclwwlk1  25838  numclwwlk2lem1  25842  numclwlk2lem2f  25843  numclwlk2lem2f1o  25845  numclwwlk2  25847  numclwwlk3  25849  numclwwlk4  25850  numclwwlk6  25853  numclwwlk7  25854  numclwwlk8  25855  frgrareg  25857  frgraregord013  25858  gxpval  25999  gxnval  26000  gxnn0neg  26003  gxnn0suc  26004  gxneg  26006  gxsuc  26012  gxnn0add  26014  gxadd  26015  gxsub  26016  gxnn0mul  26017  gxmul  26018  gxmodid  26019  gxdi  26036  zerdivemp1  26174  rngoridfz  26175  vcid  26182  vcdi  26183  vcdir  26184  vcass  26185  imsmetlem  26334  0oval  26441  ajval  26515  shlub  27079  hmopco  27688  adjlnop  27751  mdslmd4i  27998  fcoinvbr  28224  fresf1o  28240  divnumden2  28389  ressnm  28420  ress1r  28559  smatfval  28628  pstmfval  28706  pl1cn  28768  ind1  28847  ind0  28848  sigaclcuni  28947  sigagenss2  28979  measun  29040  measvuni  29043  dya2iocnrect  29109  omsmeas  29161  omsmeasOLD  29162  ballotlemieq  29355  ballotlemrv1  29359  ballotlemieqOLD  29393  ballotlemrv1OLD  29397  sgn3da  29418  bnj837  29578  bnj517  29702  bnj553  29715  bnj594  29729  bnj967  29762  bnj1097  29796  bnj1110  29797  bnj1118  29799  bnj1128  29805  bnj1125  29807  bnj1145  29808  bnj1136  29812  bnj1173  29817  bnj1189  29824  bnj1204  29827  bnj1279  29833  bnj1321  29842  bnj1413  29850  erdszelem2  29921  cnpcon  29959  cvmscld  30002  mrsubcv  30154  mrsubvr  30155  ghomf1olem  30318  iprodefisumlem  30382  dvdspw  30392  dfon2lem3  30437  dfon2lem7  30441  frrlem4  30523  nofulllem3  30599  btwndiff  30800  brcolinear2  30831  btwnconn1  30874  nn0prpwlem  30984  hmeoclda  30995  hmeocldb  30996  ivthALT  30997  fnemeet1  31028  fnejoin1  31030  nnssi3  31122  nndivsub  31123  bj-ceqsalt1  31485  onsucuni3  31772  ftc1anclem4  32022  areacirclem2  32035  areacirclem5  32038  areacirc  32039  upixp  32058  filbcmb  32069  cnresima  32098  smprngopr  32287  igenval2  32301  lsmsat  32576  lsmsatcv  32578  lsatcvatlem  32617  islshpcv  32621  l1cvpat  32622  lfli  32629  lshpset2N  32687  cvrnbtwn  32839  meetat2  32865  atcmp  32879  atcvreq0  32882  atlatmstc  32887  cvlcvr1  32907  cvlcvrp  32908  cvlatcvr2  32910  cvr2N  32978  cvratlem  32988  2atjm  33012  athgt  33023  2lplnmN  33126  2llnmj  33127  2lplnmj  33189  dalemswapyzps  33257  dalem23  33263  dalem24  33264  dalem25  33265  dalem27  33266  dalem28  33267  dalem38  33277  dalem39  33278  dalem44  33283  dalem45  33284  dalem51  33290  dalem52  33291  dalem56  33295  pmapglbx  33336  pmapjat1  33420  pmapjat2  33421  paddatclN  33516  osumcllem4N  33526  osumcllem7N  33529  ltrncoval  33712  cdleme0aa  33778  cdleme0b  33780  cdleme8  33818  cdlemesner  33864  cdleme22eALTN  33914  cdleme26eALTN  33930  cdleme35h  34025  cdleme50trn2  34120  cdleme  34129  tgrpov  34317  tendotp  34330  tendoidcl  34338  tendo0co2  34357  cdlemkvcl  34411  dvhopvadd  34663  dvhopellsm  34687  dihmeetlem1N  34860  dihmeetlem9N  34885  dihatexv  34908  lcfl7lem  35069  mapdrvallem2  35215  mapdh9a  35360  hdmapevec  35408  ismrcd1  35542  istopclsd  35544  ismrc  35545  mapfzcons  35560  eldioph2  35606  diophrex  35620  diophren  35658  pellexlem1  35675  pellexlem5  35679  pellqrexplicit  35725  reglogmul  35743  reglogexp  35744  rmxycomplete  35767  congmul  35819  congabseq  35826  acongsym  35828  acongneg2  35829  fzneg  35834  acongeq  35835  jm2.19  35850  jm2.22  35852  jm2.23  35853  jm2.20nn  35854  rmydioph  35871  rmxdiophlem  35872  jm3.1  35877  pwssplit4  35949  hbtlem2  35985  idomrootle  36071  pwinfi2  36168  relexpaddss  36312  trclimalb2  36320  brtrclfv2  36321  trclfvdecomr  36322  dvconstbi  36684  expgrowth  36685  chordthmALT  37327  wessf1ornlem  37469  disjf1o  37476  fmul01lt1lem1  37704  climsuselem1  37728  climsuse  37729  limcperiod  37750  lptre2pt  37762  cncfshift  37793  cncfperiod  37798  icccncfext  37807  dvnmptconst  37858  dvnprodlem1  37863  dvnprodlem2  37864  iblspltprt  37892  itgspltprt  37898  stoweidlem3  37920  stoweidlem16  37933  stoweidlem17  37934  stoweidlem26  37943  stoweidlem34  37952  stoweidlem57  37975  fourierdlem41  38068  fourierdlem42  38069  fourierdlem42OLD  38070  fourierdlem52  38079  fourierdlem54  38081  fourierdlem74  38101  fourierdlem75  38102  fourierdlem80  38107  fourierdlem94  38121  fourierdlem102  38129  fourierdlem114  38141  etransclem18  38174  etransclem29  38185  etransclem46  38202  rrxtopnfi  38212  sge0f1o  38283  sge0xp  38330  meadjiunlem  38364  voliunsge0lem  38371  volmea  38373  carageniuncllem1  38406  caratheodorylem1  38411  caratheodory  38413  isomenndlem  38415  hoicvr  38433  ovnsubaddlem2  38456  hoidmvlelem1  38480  hoidmvlelem2  38481  hoidmvlelem3  38482  hspmbllem2  38512  iccpartiltu  38827  icceuelpart  38841  oexpnegnz  38898  gbepos  38950  gbegt5  38953  gboage9  38956  bgoldbwt  38969  nnsum3primesgbe  38978  nnsum4primeseven  38986  nnsum4primesevenALTV  38987  bgoldbtbndlem1  38991  bgoldbtbndlem2  38992  bgoldbtbndlem3  38993  tgblthelfgott  38999  pfxnd  39029  pfxlen0  39030  pfxfv  39033  pfxeq  39038  pfxsuffeqwrdeq  39040  pfxpfx  39049  ccats1pfxeq  39055  ccats1pfxeqrex  39056  pfxccatin12lem2  39058  pfxccatpfx1  39061  pfxccatid  39064  repswpfx  39070  elpwdifsn  39083  ssprsseq  39095  fun2dmnop  39121  fpropnf1  39130  2leaddle2  39138  ssfz12  39148  fsumsplitsndif  39190  fsummmodsndifre  39191  fsummmodsnunz  39192  structiedg0val  39222  lpvtx  39257  incistruhgr  39270  upgredg2vtx  39331  upgredgpr  39332  ausgrumgri  39354  ausgrusgri  39355  usgredg2vtxeuALT  39401  ushgredgedga  39408  ushgredgedgaloop  39410  uspgr1v1eop  39426  usgr1vr  39431  usgr1v0edg  39433  uhgrissubgr  39449  egrsubgr  39451  0uhgrsubgr  39453  dfnbgr3  39510  nbupgrres  39540  nb3grprlem1  39556  cplgr3v  39604  vtxdg0e  39636  umgr2v2enb1  39665  rusgr1vtx  39705  isewlk  39721  ewlkinedg  39723  upgrewlkle2  39725  1wlk1walk  39749  1wlkvtxeledg  39773  lfgriswlk  39775  lfgr1wlknloop  39776  spthonpthon  39835  spthonepeq-av  39836  uhgr1wlkspth  39839  usgr2wlkspth  39843  1ewlk  39881  1pthon2v-av  39920  umgr2adedgwlkonALT  39948  umgr2wlkon  39951  31wlkdlem9  39961  uhgr3cyclex  39975  umgr3cyclex  39976  upgr4cycl4dv4e  39978  usgra2pth  39993  usgvincvad  40041  usgvincvadALT  40044  rngdir  40207  c0snmhm  40240  rngccatidALTV  40316  funcringcsetcALTV2lem6  40368  funcringcsetcALTV2lem9  40371  ringccatidALTV  40379  funcringcsetclem6ALTV  40391  ofaddmndmap  40450  mapprop  40452  nn0sumltlt  40456  gsumpr  40467  domnmsuppn0  40479  scmsuppss  40482  mndpsuppfi  40485  gsumlsscl  40493  ply1ass23l  40499  ply1mulgsumlem1  40503  lincfsuppcl  40531  linccl  40532  lincvalsng  40534  lincvalpr  40536  lincdifsn  40542  ellcoellss  40553  lincext1  40572  lincext2  40573  lincext3  40574  lindslinindimp2lem2  40577  ldepspr  40591  lincresunit3lem1  40597  lincresunit3lem2  40598  islindeps2  40601  logcxp0  40671  elbigo2r  40689  elbigolo1  40693  fllog2  40704  nnolog2flm1  40726  digvalnn0  40735  nn0digval  40736  dignn0fr  40737  dignn0ldlem  40738  dignnld  40739  digexp  40743  dignn0flhalflem1  40751  dignn0flhalflem2  40752  dignn0ehalf  40753  dignn0flhalf  40754
  Copyright terms: Public domain W3C validator