MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ad2antrl Structured version   Visualization version   GIF version

Theorem ad2antrl 710
Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.)
Hypothesis
Ref Expression
ad2ant.1 (𝜑𝜓)
Assertion
Ref Expression
ad2antrl ((𝜒 ∧ (𝜑𝜃)) → 𝜓)

Proof of Theorem ad2antrl
StepHypRef Expression
1 ad2ant.1 . . 3 (𝜑𝜓)
21adantr 468 . 2 ((𝜑𝜃) → 𝜓)
32adantl 469 1 ((𝜒 ∧ (𝜑𝜃)) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 198  df-an 385
This theorem is referenced by:  simprl  778  simprll  788  simprlr  789  simprl1  1274  simprl2  1276  simprl3  1278  disjxiun  4852  reusv2lem4  5083  fr2nr  5302  somin1  5753  tz7.7  5975  f1oprg  6406  soisores  6810  elovmpt2rab1  7120  sorpssi  7182  onint  7234  ordsucelsuc  7261  elxp5  7350  wemoiso  7392  wemoiso2  7393  el2xptp0  7453  ressuppss  7557  imacosupp  7579  tz7.48lem  7781  oalimcl  7886  oeeui  7928  oaabs2  7971  omabs  7973  swoer  8018  ralxpmap  8153  pw2f1olem  8312  enfixsn  8317  mapxpen  8374  mapunen  8377  unxpdomlem2  8413  unxpdomlem3  8414  findcard3  8451  isfinite2  8466  domunfican  8481  fodomfi  8487  fissuni  8519  fipreima  8520  indexfi  8522  fsuppsssupp  8539  marypha1lem  8587  marypha2  8593  supmo  8606  infmo  8649  oieu  8692  brwdom2  8726  ixpiunwdom  8744  cantnfval2  8822  cantnfle  8824  cantnflt  8825  cantnf  8846  wemapwe  8850  cnfcom  8853  rankonidlem  8947  r1pwcl  8966  eldju2ndl  9042  eldju2ndr  9043  djuun  9044  infxpenlem  9128  infxpenc2lem1  9134  fseqenlem1  9139  dfac8clem  9147  mappwen  9227  dfac3  9236  dfac5  9243  dfac12lem3  9261  cdainf  9308  infunsdom  9330  coftr  9389  ssfin4  9426  domfin4  9427  fin23lem26  9441  fin23lem22  9443  fin23lem28  9456  fin23lem32  9460  fin23lem40  9467  isf32lem5  9473  compssiso  9490  isf34lem4  9493  isfin1-3  9502  fin1a2lem13  9528  hsmexlem2  9543  hsmexlem4  9545  zorn2lem1  9612  ttukeylem6  9630  iundom2g  9656  konigthlem  9684  pwcfsdom  9699  fpwwe2lem12  9757  fpwwe2  9759  pwfseqlem3  9776  winalim2  9812  r1wunlim  9853  inttsk  9890  inar1  9891  grur1  9936  nqereq  10051  ltexprlem7  10158  prlem936  10163  00id  10505  addid2  10513  ltord1  10848  divdiv1  11030  divdiv2  11031  conjmul  11036  ltdivmul  11192  ledivmul  11193  lt2mul2div  11195  ltdiv23  11208  lediv23  11209  lediv12a  11210  ledivp1  11219  negfi  11265  nn0nndivcl  11647  nn0ge0div  11731  peano2uz2  11750  peano5uzi  11751  eluzp1m1  11947  qbtwnre  12267  xralrple  12273  xleadd1a  12320  xmulge0  12351  xmulass  12354  xlemul1a  12355  iooshf  12489  divelunit  12556  eluzgtdifelfzo  12773  modadd1  12950  modmul1  12966  seqcl2  13061  seqfveq2  13065  seqid2  13089  seqhomo  13090  seqdistr  13094  mulexpz  13142  leexp2r  13160  expnlbnd2  13237  expmulnbnd  13238  hashmap  13458  hashfun  13460  hashbclem  13472  hashfacen  13474  hashf1lem2  13476  hashf1  13477  ccatsymb  13598  swrdsb0eq  13690  swrdswrd  13703  wrdind  13719  wrd2ind  13720  swrdccatin1  13726  swrdccatin2  13730  swrdccatin12  13734  swrdccat  13736  splid  13747  repswswrd  13774  0csh0  13782  2cshw  13802  cshweqrep  13810  relexp0g  14004  relexpsucnnr  14007  relexpindlem  14045  sqrlem1  14225  sqrlem6  14230  rlim  14468  rlimclim1  14518  climsup  14642  caurcvg2  14650  caucvgb  14652  iseralt  14657  sumss  14697  fsum2dlem  14743  mptfzshft  14751  modfsummod  14767  o1fsum  14786  incexclem  14809  divrcnv  14825  flo1  14827  fprodrev  14947  fprod2dlem  14950  ruclem6  15203  moddvds  15233  dvdsaddre2b  15271  dvdsflip  15281  addmodlteqALT  15289  nn0o  15338  fldivndvdslt  15376  bitsf1ocnv  15404  bitsf1  15406  sadcaddlem  15417  bezoutlem2  15495  bezoutlem4  15497  lcmgcdlem  15557  prmind2  15635  isprm5  15655  isprm6  15662  cncongrprm  15673  hashdvds  15716  crth  15719  eulerthlem2  15723  prmdiveq  15727  hashgcdlem  15729  hashgcdeq  15730  iserodd  15776  pclem  15779  pcprendvds2  15782  pcexp  15800  pcneg  15814  pc2dvds  15819  pcmpt  15832  prmpwdvds  15844  pockthg  15846  prmreclem5  15860  4sqlem11  15895  ramub2  15954  ramubcl  15958  ram0  15962  ramub1lem2  15967  ramcl  15969  prmgaplem3  15993  prmgaplem6  15996  setscom  16133  sscpwex  16698  initoeu2  16889  setcinv  16963  funcestrcsetclem9  17012  funcsetcestrclem9  17027  fullsetcestrc  17030  1stfcl  17061  2ndfcl  17062  hofpropd  17131  isacs3lem  17390  isacs4lem  17392  acsmap2d  17403  submnd0  17544  subsubm  17581  frmdup1  17625  frmdup3lem  17627  sgrp2nmndlem2  17635  isgrpinv  17696  subsubg  17838  cycsubgcl  17841  conjghm  17912  qusghm  17918  gsumwrev  18016  symgfixelsi  18075  symgsssg  18107  symgfisg  18108  psgnunilem2  18135  odf1o2  18208  sylow1lem1  18233  odcau  18239  pgpfi  18240  pgpssslw  18249  fislw  18260  efgtlen  18359  efginvrel2  18360  efgrelexlemb  18383  efgredeu  18385  efgcpbllemb  18388  frgpup1  18408  cygabl  18512  lt6abl  18516  gsum2d  18591  gsum2d2lem  18592  gsum2d2  18593  telgsumfzslem  18606  dmdprdsplit2lem  18665  ablfacrp  18686  pgpfac1lem3  18697  gsummgp0  18829  irredrmul  18928  subsubrg  19029  islss4  19188  lspextmo  19282  lspsnat  19372  issubassa  19552  resspsradd  19644  resspsrmul  19645  coe1tmmul2  19873  pf1ind  19946  prmirredlem  20068  znf1o  20126  znidomb  20136  frgpcyg  20148  psgnghm  20152  psgndiflemB  20173  frlmlbs  20366  frlmup1  20367  lindfind  20385  islindf3  20395  lindfmm  20396  mamulid  20477  mat1dimelbas  20508  mdetdiaglem  20635  mdetralt2  20646  mndifsplit  20673  smadiadetglem2  20710  1elcpmat  20753  pmatcollpw3lem  20821  chfacfisf  20892  chfacfisfcpmat  20893  chfacffsupp  20894  chfacfscmulfsupp  20897  chfacfscmulgsum  20898  chfacfpmmulfsupp  20901  chfacfpmmulgsum  20902  cayhamlem1  20904  cpmadugsumlemF  20914  cayleyhamilton1  20930  tgcl  21007  pptbas  21046  clsval2  21088  mretopd  21130  lmbr2  21297  cncls2  21311  nrmsep  21395  regsep2  21414  cmpsublem  21436  cmpsub  21437  tgcmp  21438  uncmp  21440  hauscmplem  21443  iunconnlem  21464  1stcrest  21490  2ndcctbss  21492  2ndcsep  21496  dis2ndc  21497  hausllycmp  21531  dislly  21534  kgentopon  21575  1stckgen  21591  kgencn3  21595  ptpjpre1  21608  ptbasin  21614  ptpjopn  21649  dfac14  21655  ptcnplem  21658  txcn  21663  txindis  21671  txdis1cn  21672  ptrescn  21676  txcmplem1  21678  txcmp  21680  txhaus  21684  txlm  21685  tx1stc  21687  txkgen  21689  xkococn  21697  qtopcn  21751  kqreglem1  21778  kqreglem2  21779  kqnrmlem1  21780  kqnrmlem2  21781  hmeoimaf1o  21807  reghmph  21830  nrmhmph  21831  txhmeo  21840  ptuncnv  21844  filconn  21920  fbasrn  21921  fmfnfmlem2  21992  flimfnfcls  22065  cnpfcfi  22077  alexsublem  22081  alexsubALTlem2  22085  alexsubALTlem3  22086  alexsubALTlem4  22087  alexsubALT  22088  ptcmplem3  22091  cnextfval  22099  tsmsxp  22191  imasdsf1olem  22411  bl2in  22438  blssps  22462  blss  22463  blssexps  22464  blssex  22465  blcld  22543  stdbdxmet  22553  met1stc  22559  prdsxmslem2  22567  metcnp3  22578  metcnpi3  22584  txmetcnp  22585  nmo0  22772  nmoid  22779  icccmplem1  22858  icccmp  22861  xrge0tsms  22870  metdseq0  22890  cnheiborlem  22986  cnheibor  22987  cnllycmp  22988  pcoval2  23048  cmetcaulem  23319  iscmet3lem1  23322  iscmet3lem2  23323  equivcau  23331  lmcau  23344  cncmet  23352  ivthlem2  23455  ivthlem3  23456  ovoliunlem2  23506  ovolscalem2  23517  uniioombl  23592  dyaddisj  23599  opnmbllem  23604  volivth  23610  ismbfd  23642  ismbf3d  23657  mbfimaopnlem  23658  mbfinf  23668  itg1addlem4  23702  mbfi1fseqlem1  23718  mbfi1fseqlem3  23720  mbfi1fseqlem4  23721  mbfi1fseqlem5  23722  mbfi1fseqlem6  23723  itg2seq  23745  itg2lea  23747  itg2split  23752  itg2cnlem1  23764  limciun  23894  dvmptfsum  23974  rolle  23989  c1lip1  23996  dvcnvrelem1  24016  dvcnvre  24018  dvcvx  24019  itgsubst  24048  tdeglem4  24056  mdegmullem  24074  plyco0  24184  coemullem  24242  dgreq0  24257  dgrmul  24262  dgrco  24267  elqaalem2  24311  aannenlem1  24319  aaliou3lem9  24341  ulmres  24378  ulmshftlem  24379  angneg  24769  dcubic  24809  cxploglim  24940  cxploglim2  24941  scvxcvx  24948  lgamgulmlem5  24995  lgamcvg2  25017  basellem3  25045  basellem4  25046  sqff1o  25144  fsumdvdsdiaglem  25145  dvdsflsumcom  25150  dvdsmulf1o  25156  fsumvma2  25175  logfac2  25178  logfacrlim  25185  logexprlim  25186  dchrelbasd  25200  lgsne0  25296  lgsqrlem2  25308  lgsqrmodndvds  25314  gausslemma2dlem1a  25326  lgseisenlem2  25337  lgsquadlem1  25341  lgsquadlem2  25342  lgsquadlem3  25343  lgsquad2lem2  25346  2sqlem8  25387  2sqlem11  25390  chpo1ubb  25406  vmadivsum  25407  rplogsumlem2  25410  rpvmasumlem  25412  dchrmusum2  25419  dchrvmasumlem1  25420  dchrisum0fno1  25436  dchrisum0re  25438  dchrisum0lem1  25441  dchrisum0lem2  25443  dchrisum0lem3  25444  dchrisum0  25445  mulogsumlem  25456  mulog2sumlem2  25460  vmalogdivsum2  25463  logsqvma  25467  log2sumbnd  25469  selberglem3  25472  selberg  25473  selberg2lem  25475  selberg2b  25477  selberg3lem2  25483  pntrmax  25489  pntrsumo1  25490  pntlemn  25525  pntlemp  25535  qabvle  25550  ostthlem1  25552  ostthlem2  25553  ostth2lem2  25559  ostth3  25563  idmot  25668  iscgra1  25938  brbtwn2  26021  colinearalglem4  26025  colinearalg  26026  ax5seglem9  26053  axpaschlem  26056  axcontlem2  26081  axcontlem7  26086  axcontlem8  26087  eengtrkg  26101  upgr1eopALT  26248  uspgredg2vlem  26352  subumgr  26418  nbgr0vtxlem  26489  edgnbusgreu  26506  edgnbusgreuOLD  26507  nb3grprlem1  26520  wlkl1loop  26784  pthdivtx  26875  usgr2pth  26910  crctcshwlkn0  26964  wlklnwwlkln1  27017  wwlksnext  27052  clwwlkccatlem  27154  clwlkclwwlklem2a  27163  clwwlkinwwlk  27211  clwwlkn1loopb  27214  clwwlkf  27218  wwlksubclwwlk  27231  clwwlknscsh  27235  clwwlknon1  27287  1conngr  27389  n4cyclfrgr  27488  numclwwlk2lem1lem  27540  2clwwlk2clwwlk  27549  numclwwlk1lem2f1  27558  numclwlk1lem1  27571  numclwwlk2lem1  27578  numclwlk2lem2f  27579  numclwwlk2lem1OLD  27585  numclwlk2lem2fOLD  27586  numclwwlk7  27601  frgrogt3nreg  27607  grpoidinvlem1  27709  grpoidinvlem3  27711  grporcan  27723  nmlnoubi  28001  blocnilem  28009  ipblnfi  28061  htthlem  28124  ocsh  28492  shmodsi  28598  pjhthlem2  28601  5oalem2  28864  eigposi  29045  nmopub2tALT  29118  nmfnleub2  29135  nmcexi  29235  nmopcoi  29304  kbass3  29327  mdslmd1lem1  29534  mdslmd1lem2  29535  chirredlem2  29600  chirredlem4  29602  mdsymlem3  29614  mdsymlem5  29616  sumdmdii  29624  sumdmdlem  29627  sumdmdlem2  29628  foresf1o  29690  disjxpin  29748  1stpreimas  29832  resf1o  29854  gsumvsca1  30129  gsumvsca2  30130  xrge0tsmsd  30132  mdetpmtr1  30236  mdetpmtr2  30237  pstmxmet  30287  qqhghm  30379  qqhrhm  30380  esumpcvgval  30487  volmeas  30641  imambfm  30671  dya2iocnrect  30690  oddpwdc  30763  sseqf  30801  orvcgteel  30876  orvclteel  30881  ballotlemsf1o  30922  bnj1110  31394  bnj1118  31396  txpconn  31558  connpconn  31561  cnllysconn  31571  rellysconn  31577  cvmsss2  31600  cvmlift2lem9  31637  mrsubfval  31749  mppsval  31813  dfon2lem6  32034  trpredmintr  32072  wzel  32111  sltres  32157  nosupno  32191  nosupbnd2  32204  sslttr  32256  ifscgr  32493  cgrxfr  32504  btwnconn1lem5  32540  btwnconn1lem6  32541  btwnconn1lem12  32547  brsegle  32557  finminlem  32654  gtinfOLD  32656  nn0prpwlem  32659  fnessref  32694  refssfne  32695  neibastop1  32696  topjoin  32702  fnemeet2  32704  bj-finsumval0  33482  topdifinffinlem  33529  cnfinltrel  33575  matunitlindflem2  33737  poimirlem28  33768  poimirlem32  33772  opnmbllem0  33776  mblfinlem1  33777  mblfinlem4  33780  ismblfin  33781  mbfresfi  33786  itg2addnclem  33791  itg2addnclem3  33793  itg2addnc  33794  bddiblnc  33810  unirep  33837  frinfm  33860  sdclem2  33867  geomcau  33884  istotbnd3  33899  sstotbnd2  33902  sstotbnd  33903  sstotbnd3  33904  totbndbnd  33917  cntotbnd  33924  ismtyres  33936  heibor1lem  33937  heiborlem1  33939  heiborlem8  33946  ismndo1  34001  isdivrngo  34078  unichnidl  34159  cvlcvr1  35137  ishlat3N  35152  llnmlplnN  35337  islvol2aN  35390  4atlem4c  35399  4atlem4d  35400  isline2  35572  isline3  35574  linepsubclN  35749  lhpexle3lem  35809  lhpjat2  35819  cdlemd4  35999  cdleme0cq  36013  cdleme32fva  36235  cdleme32fvaw  36237  tendo0mul  36624  tendo0mulr  36625  diameetN  36854  dvhvaddcl  36893  dvhvaddcomN  36894  cdlemm10N  36916  dvadiaN  36926  djavalN  36933  dihvalcqat  37037  dihopelvalcpre  37046  djhval  37196  dihjat1lem  37226  elrfi  37776  nacsfix  37794  fzsplit1nn0  37836  eldioph2  37844  lzenom  37852  irrapxlem3  37907  pellexlem5  37916  pell1234qrne0  37936  pell1234qrmulcl  37938  pell14qrdich  37952  pell1qrge1  37953  pellqrex  37962  reglogltb  37974  reglogleb  37975  rmxypairf1o  37994  rmxycomplete  38000  monotoddzzfi  38025  congadd  38051  congsym  38053  acongrep  38065  jm2.19lem3  38076  jm2.19lem4  38077  jm2.22  38080  jm2.25  38084  expdiophlem1  38106  wepwsolem  38130  kelac1  38151  lmhmfgsplit  38174  pwslnm  38182  hbtlem6  38217  hbt  38218  mon1psubm  38302  deg1mhm  38303  iunrelexp0  38511  dssmapnvod  38831  gsumws3  39016  gsumws4  39017  mulltgt0  39692  fnchoice  39699  disjrnmpt2  39881  fzisoeu  40012  fsumiunss  40304  climinf  40335  mullimc  40345  mullimcf  40352  stoweidlem14  40727  stoweidlem17  40730  stoweidlem34  40747  stoweidlem50  40763  fourierdlem42  40862  fourierdlem62  40881  fourierdlem71  40890  fourierdlem76  40895  qndenserrnbllem  41010  subsaliuncl  41072  sge0resplit  41119  iccpartigtl  41951  ccatpfx  42001  pfxccatin12lem2  42016  pfxccatin12  42017  prmdvdsfmtnof1lem2  42089  bgoldbtbndlem3  42287  bgoldbtbnd  42289  uspgrsprf1  42340  subsubmgm  42382  isassintop  42431  2zlidl  42519  2zrngnmrid  42535  rngcinv  42566  rngcinvALTV  42578  ringcinv  42617  funcringcsetcALTV2lem9  42629  ringcinvALTV  42641  funcringcsetclem9ALTV  42652  fldhmsubc  42669  fldhmsubcALTV  42687  mndpsuppss  42737  gsumlsscl  42749  lincsum  42803  lindslinindsimp1  42831  lindslinindimp2lem4  42835  lincresunitlem2  42850  elfzolborelfzop1  42894  elbigo2  42931  digexp  42986  dig1  42987  nn0sumshdiglemB  42999
  Copyright terms: Public domain W3C validator