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

Theorem ad2antrl 759
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 479 . 2 ((𝜑𝜃) → 𝜓)
32adantl 480 1 ((𝜒 ∧ (𝜑𝜃)) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 195  df-an 384
This theorem is referenced by:  simprl  789  simprll  797  simprlr  798  disjxiun  4573  reusv2lem4  4792  fr2nr  5005  somin1  5434  tz7.7  5651  f1oprg  6077  soisores  6454  elovmpt2rab1  6756  sorpssi  6818  onint  6864  ordsucelsuc  6891  elxp5  6981  wemoiso  7021  wemoiso2  7022  el2xptp0  7080  ressuppss  7178  imacosupp  7199  tz7.48lem  7400  oalimcl  7504  oeeui  7546  oaabs2  7589  omabs  7591  swoer  7636  0erOLD  7645  ralxpmap  7770  pw2f1olem  7926  enfixsn  7931  mapxpen  7988  mapunen  7991  unxpdomlem2  8027  unxpdomlem3  8028  findcard3  8065  isfinite2  8080  domunfican  8095  fodomfi  8101  fissuni  8131  fipreima  8132  indexfi  8134  fsuppsssupp  8151  marypha1lem  8199  marypha2  8205  supmo  8218  infmo  8261  oieu  8304  brwdom2  8338  ixpiunwdom  8356  cantnfval2  8426  cantnfle  8428  cantnflt  8429  cantnf  8450  wemapwe  8454  cnfcom  8457  rankonidlem  8551  r1pwcl  8570  infxpenlem  8696  infxpenc2lem1  8702  fseqenlem1  8707  dfac8clem  8715  mappwen  8795  dfac3  8804  dfac5  8811  dfac12lem3  8827  cdainf  8874  infunsdom  8896  coftr  8955  ssfin4  8992  domfin4  8993  fin23lem26  9007  fin23lem22  9009  fin23lem28  9022  fin23lem32  9026  fin23lem40  9033  isf32lem5  9039  compssiso  9056  isf34lem4  9059  isfin1-3  9068  fin1a2lem13  9094  hsmexlem2  9109  hsmexlem4  9111  zorn2lem1  9178  ttukeylem6  9196  iundom2g  9218  konigthlem  9246  pwcfsdom  9261  fpwwe2lem12  9319  fpwwe2  9321  pwfseqlem3  9338  winalim2  9374  r1wunlim  9415  inttsk  9452  inar1  9453  grur1  9498  nqereq  9613  ltexprlem7  9720  prlem936  9725  00id  10062  addid2  10070  ltord1  10405  divdiv1  10587  divdiv2  10588  conjmul  10593  ltdivmul  10749  ledivmul  10750  lt2mul2div  10752  ltdiv23  10765  lediv23  10766  lediv12a  10767  ledivp1  10776  negfi  10822  nn0nndivcl  11211  nn0ge0div  11280  peano2uz2  11299  peano5uzi  11300  eluzp1m1  11545  qbtwnre  11865  xralrple  11871  xleadd1a  11914  xmulge0  11945  xmulass  11948  xlemul1a  11949  iooshf  12081  divelunit  12143  eluzgtdifelfzo  12354  modadd1  12526  modmul1  12542  seqcl2  12638  seqfveq2  12642  seqid2  12666  seqhomo  12667  seqdistr  12671  mulexpz  12719  leexp2r  12737  expnlbnd2  12814  expmulnbnd  12815  hashmap  13036  hashfun  13038  hashbclem  13047  hashfacen  13049  hashf1lem2  13051  hashf1  13052  ccatsymb  13167  swrdsb0eq  13247  swrdswrd  13260  wrdind  13276  wrd2ind  13277  swrdccatin1  13282  swrdccatin2  13286  swrdccatin12  13290  swrdccat  13292  splid  13303  repswswrd  13330  0csh0  13338  2cshw  13358  cshweqrep  13366  relexp0g  13558  relexpsucnnr  13561  relexpindlem  13599  sqrlem1  13779  sqrlem6  13784  rlim  14022  rlimclim1  14072  climsup  14196  caurcvg2  14204  caucvgb  14206  iseralt  14211  sumss  14250  fsum2dlem  14291  mptfzshft  14300  modfsummod  14315  o1fsum  14334  incexclem  14355  divrcnv  14371  flo1  14373  fprodrev  14494  fprod2dlem  14497  ruclem6  14751  moddvds  14777  dvdsaddre2b  14815  dvdsflip  14825  addmodlteqALT  14833  fldivndvdslt  14924  bitsf1ocnv  14952  bitsf1  14954  sadcaddlem  14965  bezoutlem2  15043  bezoutlem4  15045  lcmgcdlem  15105  prmind2  15184  isprm5  15205  isprm6  15212  cncongrprm  15223  hashdvds  15266  crth  15269  eulerthlem2  15273  prmdiveq  15277  hashgcdlem  15279  hashgcdeq  15280  iserodd  15326  pclem  15329  pcprendvds2  15332  pcexp  15350  pcneg  15364  pc2dvds  15369  pcmpt  15382  prmpwdvds  15394  pockthg  15396  prmreclem5  15410  4sqlem11  15445  ramub2  15504  ramubcl  15508  ram0  15512  ramub1lem2  15517  ramcl  15519  prmgaplem3  15543  prmgaplem6  15546  setscom  15679  sscpwex  16246  initoeu2  16437  setcinv  16511  funcestrcsetclem9  16559  funcsetcestrclem9  16574  fullsetcestrc  16577  1stfcl  16608  2ndfcl  16609  hofpropd  16678  isacs3lem  16937  isacs4lem  16939  acsmap2d  16950  submnd0  17091  subsubm  17128  frmdup1  17172  frmdup3lem  17174  sgrp2nmndlem2  17182  isgrpinv  17243  subsubg  17388  cycsubgcl  17391  conjghm  17462  qusghm  17468  gsumwrev  17567  symgfixelsi  17626  symgsssg  17658  symgfisg  17659  psgnunilem2  17686  odf1o2  17759  sylow1lem1  17784  odcau  17790  pgpfi  17791  pgpssslw  17800  fislw  17811  efgtlen  17910  efginvrel2  17911  efgrelexlemb  17934  efgredeu  17936  efgcpbllemb  17939  frgpup1  17959  cygabl  18063  lt6abl  18067  gsum2d  18142  gsum2d2lem  18143  gsum2d2  18144  telgsumfzslem  18156  dmdprdsplit2lem  18215  ablfacrp  18236  pgpfac1lem3  18247  gsummgp0  18379  irredrmul  18478  subsubrg  18577  islss4  18731  lspextmo  18825  lspsnat  18914  issubassa  19093  resspsradd  19185  resspsrmul  19186  coe1tmmul2  19415  pf1ind  19488  prmirredlem  19607  znf1o  19666  znidomb  19676  frgpcyg  19688  psgnghm  19692  psgndiflemB  19712  frlmlbs  19902  frlmup1  19903  lindfind  19921  islindf3  19931  lindfmm  19932  mamulid  20013  mat1dimelbas  20043  mdetdiaglem  20170  mdetralt2  20181  mndifsplit  20208  smadiadetglem2  20244  1elcpmat  20286  pmatcollpw3lem  20354  chfacfisf  20425  chfacfisfcpmat  20426  chfacffsupp  20427  chfacfscmulfsupp  20430  chfacfscmulgsum  20431  chfacfpmmulfsupp  20434  chfacfpmmulgsum  20435  cayhamlem1  20437  cpmadugsumlemF  20447  cayleyhamilton1  20463  tgcl  20531  pptbas  20569  clsval2  20611  mretopd  20653  lmbr2  20820  cncls2  20834  nrmsep  20918  regsep2  20937  cmpsublem  20959  cmpsub  20960  tgcmp  20961  uncmp  20963  hauscmplem  20966  iunconlem  20987  1stcrest  21013  2ndcctbss  21015  2ndcsep  21019  dis2ndc  21020  hausllycmp  21054  dislly  21057  kgentopon  21098  1stckgen  21114  kgencn3  21118  ptpjpre1  21131  ptbasin  21137  ptpjopn  21172  dfac14  21178  ptcnplem  21181  txcn  21186  txindis  21194  txdis1cn  21195  ptrescn  21199  txcmplem1  21201  txcmp  21203  txhaus  21207  txlm  21208  tx1stc  21210  txkgen  21212  xkococn  21220  qtopcn  21274  kqreglem1  21301  kqreglem2  21302  kqnrmlem1  21303  kqnrmlem2  21304  hmeoimaf1o  21330  reghmph  21353  nrmhmph  21354  txhmeo  21363  ptuncnv  21367  filcon  21444  fbasrn  21445  fmfnfmlem2  21516  flimfnfcls  21589  cnpfcfi  21601  alexsublem  21605  alexsubALTlem2  21609  alexsubALTlem3  21610  alexsubALTlem4  21611  alexsubALT  21612  ptcmplem3  21615  cnextfval  21623  tsmsxp  21715  imasdsf1olem  21935  bl2in  21962  blssps  21986  blss  21987  blssexps  21988  blssex  21989  blcld  22067  stdbdxmet  22077  met1stc  22083  prdsxmslem2  22091  metcnp3  22102  metcnpi3  22108  txmetcnp  22109  nmo0  22296  nmoid  22303  icccmplem1  22380  icccmp  22383  xrge0tsms  22392  metdseq0  22412  cnheiborlem  22508  cnheibor  22509  cnllycmp  22510  pcoval2  22571  cmetcaulem  22838  iscmet3lem1  22841  iscmet3lem2  22842  equivcau  22850  lmcau  22863  cncmet  22871  ivthlem2  22972  ivthlem3  22973  ovoliunlem2  23022  ovolscalem2  23033  uniioombl  23107  dyaddisj  23114  opnmbllem  23119  volivth  23125  ismbfd  23157  ismbf3d  23171  mbfimaopnlem  23172  mbfinf  23182  itg1addlem4  23216  mbfi1fseqlem1  23232  mbfi1fseqlem3  23234  mbfi1fseqlem4  23235  mbfi1fseqlem5  23236  mbfi1fseqlem6  23237  itg2seq  23259  itg2lea  23261  itg2split  23266  itg2cnlem1  23278  limciun  23408  dvmptfsum  23486  rolle  23501  c1lip1  23508  dvcnvrelem1  23528  dvcnvre  23530  dvcvx  23531  itgsubst  23560  tdeglem4  23568  mdegmullem  23586  plyco0  23696  coemullem  23754  dgreq0  23769  dgrmul  23774  dgrco  23779  elqaalem2  23823  aannenlem1  23831  aaliou3lem9  23853  ulmres  23890  ulmshftlem  23891  angneg  24277  dcubic  24317  cxploglim  24448  cxploglim2  24449  scvxcvx  24456  lgamgulmlem5  24503  lgamcvg2  24525  basellem3  24553  basellem4  24554  sqff1o  24652  fsumdvdsdiaglem  24653  dvdsflsumcom  24658  dvdsmulf1o  24664  fsumvma2  24683  logfac2  24686  logfacrlim  24693  logexprlim  24694  dchrelbasd  24708  lgsne0  24804  lgsqrlem2  24816  lgsqrmodndvds  24822  gausslemma2dlem1a  24834  lgseisenlem2  24845  lgsquadlem1  24849  lgsquadlem2  24850  lgsquadlem3  24851  lgsquad2lem2  24854  2sqlem8  24895  2sqlem11  24898  chpo1ubb  24914  vmadivsum  24915  rplogsumlem2  24918  rpvmasumlem  24920  dchrmusum2  24927  dchrvmasumlem1  24928  dchrisum0fno1  24944  dchrisum0re  24946  dchrisum0lem1  24949  dchrisum0lem2  24951  dchrisum0lem3  24952  dchrisum0  24953  mulogsumlem  24964  mulog2sumlem2  24968  vmalogdivsum2  24971  logsqvma  24975  log2sumbnd  24977  selberglem3  24980  selberg  24981  selberg2lem  24983  selberg2b  24985  selberg3lem2  24991  pntrmax  24997  pntrsumo1  24998  pntlemn  25033  pntlemp  25043  qabvle  25058  ostthlem1  25060  ostthlem2  25061  ostth2lem2  25067  ostth3  25071  idmot  25177  iscgra1  25447  brbtwn2  25530  colinearalglem4  25534  colinearalg  25535  ax5seglem9  25562  axpaschlem  25565  axcontlem2  25590  axcontlem7  25595  axcontlem8  25596  eengtrkg  25610  umgra1  25648  uslgra1  25694  nb3graprlem1  25773  nbcusgra  25785  uvtxnbgravtx  25816  wlkntrllem3  25884  vfwlkniswwlkn  26027  wwlknext  26045  clwlkisclwwlklem2a  26106  clwwlkf  26115  clwwlknscsh  26140  clwlkfoclwwlk  26165  vdgrf  26218  iseupa  26285  eupai  26287  n4cyclfrgra  26338  frgrawopreg  26369  2spotdisj  26381  clwwlkextfrlem1  26396  extwwlkfablem2  26398  numclwwlkovf2ex  26406  numclwlk1lem2f1  26414  numclwwlk2lem1  26422  numclwlk2lem2f  26423  numclwwlk6  26433  numclwwlk7  26434  frgraogt3nreg  26440  grpoidinvlem1  26535  grpoidinvlem3  26537  grporcan  26549  nmlnoubi  26828  blocnilem  26836  ipblnfi  26888  htthlem  26951  ocsh  27319  shmodsi  27425  pjhthlem2  27428  5oalem2  27691  eigposi  27872  nmopub2tALT  27945  nmfnleub2  27962  nmcexi  28062  nmopcoi  28131  kbass3  28154  mdslmd1lem1  28361  mdslmd1lem2  28362  chirredlem2  28427  chirredlem4  28429  mdsymlem3  28441  mdsymlem5  28443  sumdmdii  28451  sumdmdlem  28454  sumdmdlem2  28455  foresf1o  28520  disjxpin  28576  1stpreimas  28659  resf1o  28686  gsumvsca1  28906  gsumvsca2  28907  xrge0tsmsd  28909  mdetpmtr1  29010  mdetpmtr2  29011  pstmxmet  29061  qqhghm  29153  qqhrhm  29154  esumpcvgval  29260  volmeas  29414  imambfm  29444  dya2iocnrect  29463  oddpwdc  29536  sseqf  29574  orvcgteel  29649  orvclteel  29654  ballotlemsf1o  29695  bnj1110  30097  bnj1118  30099  txpcon  30261  conpcon  30264  cnllyscon  30274  rellyscon  30280  cvmsss2  30303  cvmlift2lem9  30340  mrsubfval  30452  mppsval  30516  dfon2lem6  30730  trpredmintr  30768  wzel  30808  wzelOLD  30809  sltres  30854  ifscgr  31114  cgrxfr  31125  btwnconn1lem5  31161  btwnconn1lem6  31162  btwnconn1lem12  31168  brsegle  31178  finminlem  31275  gtinfOLD  31277  nn0prpwlem  31280  fnessref  31315  refssfne  31316  neibastop1  31317  topjoin  31323  fnemeet2  31325  bj-finsumval0  32107  topdifinffinlem  32154  matunitlindflem2  32359  poimirlem28  32390  poimirlem32  32394  opnmbllem0  32398  mblfinlem1  32399  mblfinlem4  32402  ismblfin  32403  mbfresfi  32409  itg2addnclem  32414  itg2addnclem3  32416  itg2addnc  32417  bddiblnc  32433  unirep  32460  frinfm  32483  sdclem2  32491  geomcau  32508  istotbnd3  32523  sstotbnd2  32526  sstotbnd  32527  sstotbnd3  32528  totbndbnd  32541  cntotbnd  32548  ismtyres  32560  heibor1lem  32561  heiborlem1  32563  heiborlem8  32570  ismndo1  32625  isdivrngo  32702  unichnidl  32783  cvlcvr1  33427  ishlat3N  33442  llnmlplnN  33626  islvol2aN  33679  4atlem4c  33688  4atlem4d  33689  isline2  33861  isline3  33863  linepsubclN  34038  lhpexle3lem  34098  lhpjat2  34108  cdlemd4  34289  cdleme0cq  34303  cdleme32fva  34526  cdleme32fvaw  34528  tendo0mul  34915  tendo0mulr  34916  diameetN  35146  dvhvaddcl  35185  dvhvaddcomN  35186  cdlemm10N  35208  dvadiaN  35218  djavalN  35225  dihvalcqat  35329  dihopelvalcpre  35338  djhval  35488  dihjat1lem  35518  elrfi  36058  nacsfix  36076  fzsplit1nn0  36118  eldioph2  36126  lzenom  36134  irrapxlem3  36189  pellexlem5  36198  pell1234qrne0  36218  pell1234qrmulcl  36220  pell14qrdich  36234  pell1qrge1  36235  pellqrex  36244  reglogltb  36256  reglogleb  36257  rmxypairf1o  36277  rmxycomplete  36283  monotoddzzfi  36308  congadd  36334  congsym  36336  acongrep  36348  jm2.19lem3  36359  jm2.19lem4  36360  jm2.22  36363  jm2.25  36367  expdiophlem1  36389  wepwsolem  36413  kelac1  36434  lmhmfgsplit  36457  pwslnm  36465  hbtlem6  36501  hbt  36502  mon1psubm  36586  deg1mhm  36587  iunrelexp0  36796  dssmapnvod  37117  gsumws3  37304  gsumws4  37305  mulltgt0  37987  fnchoice  37994  disjrnmpt2  38153  fzisoeu  38238  fsumiunss  38425  climinf  38456  mullimc  38466  mullimcf  38473  stoweidlem14  38690  stoweidlem17  38693  stoweidlem34  38710  stoweidlem50  38726  fourierdlem42  38825  fourierdlem62  38844  fourierdlem71  38853  fourierdlem76  38858  qndenserrnbllem  38973  subsaliuncl  39035  sge0resplit  39082  iccpartigtl  39745  prmdvdsfmtnof1lem2  39819  bgoldbtbndlem3  40007  bgoldbtbnd  40009  ccatpfx  40056  pfxccatin12lem2  40071  pfxccatin12  40072  upgr1eopALT  40323  uspgredg2vlem  40431  subumgr  40493  edgnbusgreu  40576  nb3grprlem1  40589  1wlkl1loop  40823  pthdivtx  40916  usgr2pth  40951  crctcsh1wlkn0  41005  1wlklnwwlkln1  41046  wwlksnext  41080  clwlkclwwlklem2a  41188  clwwlksf  41203  wwlksubclwwlks  41213  clwwnisshclwwsn  41218  clwwlksnscsh  41228  1conngr  41342  n4cyclfrgr  41442  frgrwopreg  41467  frgrhash2wsp  41478  av-numclwwlkovf2ex  41498  av-numclwlk1lem2f1  41505  av-numclwwlk2lem1  41513  av-numclwlk2lem2f  41514  av-numclwwlk7  41526  av-frgraogt3nreg  41532  subsubmgm  41568  isassintop  41617  2zlidl  41705  2zrngnmrid  41721  rngcinv  41754  rngcinvALTV  41766  ringcinv  41805  funcringcsetcALTV2lem9  41817  ringcinvALTV  41829  funcringcsetclem9ALTV  41840  fldhmsubc  41857  fldhmsubcALTV  41876  mndpsuppss  41927  gsumlsscl  41939  lincsum  41993  lindslinindsimp1  42021  lindslinindimp2lem4  42025  lincresunitlem2  42040  elfzolborelfzop1  42084  elbigo2  42125  digexp  42180  dig1  42181  nn0sumshdiglemB  42193
  Copyright terms: Public domain W3C validator