Theorem ad2antrl 735

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

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	adantl 483	. 2 ⊢ ((𝜒 ∧ 𝜑) → 𝜓)
3	2	adantrr 724	1 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜃)) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 397

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 209  df-an 398

This theorem is referenced by:  simprl  777  simprll  785  simprlr  786  simprl1  1226  simprl2  1227  simprl3  1228  disjxiun  5072  reusv2lem4  5333  axprlem5OLD  5363  fr2nr  5598  somin1  6090  tz7.7  6340  f1oprg  6817  soisores  7275  elovmporab1w  7607  elovmporab1  7608  sorpssi  7676  onint  7737  ordsucelsuc  7766  elxp5  7867  resf1extb  7878  f1oabexg  7886  wemoiso  7919  wemoiso2  7920  el2xptp0  7982  mpof1o2d  8069  frxp2  8088  frxp3  8095  ressuppss  8127  fprlem1  8244  tz7.48lem  8374  oalimcl  8489  oeeui  8532  nnaordex2  8569  oaabs2  8579  omabs  8581  swoer  8669  ralxpmap  8838  pw2f1olem  9013  enfixsn  9018  mapxpen  9075  mapunen  9078  php  9135  unxpdomlem2  9161  unxpdomlem3  9162  isfinite2  9202  fodomfi  9216  domunfican  9226  fodomfiOLD  9234  fissuni  9261  fipreima  9262  indexfi  9264  fsuppsssupp  9288  marypha1lem  9340  marypha2  9346  supmo  9359  infmo  9404  oieu  9448  brwdom2  9482  ixpiunwdom  9499  cantnfval2  9585  cantnfle  9587  cantnflt  9588  cantnf  9609  wemapwe  9613  cnfcom  9616  frrlem15  9676  rankonidlem  9747  r1pwcl  9766  eldju2ndl  9843  eldju2ndr  9844  djuun  9845  infxpenlem  9930  infxpenc2lem1  9936  fseqenlem1  9941  dfac8clem  9949  mappwen  10029  dfac3  10038  dfac5  10046  dfac12lem3  10063  infunsdom  10130  coftr  10190  ssfin4  10227  domfin4  10228  fin23lem26  10242  fin23lem22  10244  fin23lem28  10257  fin23lem32  10261  fin23lem40  10268  isf32lem5  10274  compssiso  10291  isf34lem4  10294  isfin1-3  10303  fin1a2lem13  10329  hsmexlem2  10344  hsmexlem4  10346  zorn2lem1  10413  ttukeylem6  10431  iundom2g  10457  konigthlem  10486  pwcfsdom  10501  fpwwe2lem11  10559  fpwwe2  10561  pwfseqlem3  10578  winalim2  10614  r1wunlim  10655  inttsk  10692  inar1  10693  grur1  10738  nqereq  10853  ltexprlem7  10960  prlem936  10965  00id  11316  addlid  11324  ltord1  11671  divdiv1  11861  divdiv2  11862  conjmul  11867  ltdivmul  12026  ledivmul  12027  lt2mul2div  12029  ltdiv23  12042  lediv23  12043  lediv12a  12044  ledivp1  12053  negfi  12100  nn0nndivcl  12504  nn0ge0div  12593  peano2uz2  12612  peano5uzi  12613  eluzp1m1  12809  qbtwnre  13146  xralrple  13152  xleadd1a  13200  xmulge0  13231  xmulass  13234  xlemul1a  13235  iooshf  13374  divelunit  13442  eluzgtdifelfzo  13677  modadd1  13862  modmul1  13881  seqcl2  13977  seqfveq2  13981  seqid2  14005  seqhomo  14006  seqdistr  14010  mulexpz  14059  leexp2r  14131  expnlbnd2  14191  expmulnbnd  14192  hashmap  14392  hashfun  14394  hashbclem  14409  hashfacen  14411  hashf1lem2  14413  hashf1  14414  ccatsymb  14540  swrdwrdsymb  14620  swrdsb0eq  14621  ccatpfx  14658  swrdswrd  14662  wrdind  14679  wrd2ind  14680  swrdccatin1  14682  swrdccatin2  14686  pfxccatin12lem2  14688  pfxccatin12  14690  swrdccat  14692  repswswrd  14741  0csh0  14750  cshwidxmod  14760  2cshw  14770  cshweqrep  14778  relexp0g  14979  relexpsucnnr  14982  relexpindlem  15020  01sqrexlem1  15199  01sqrexlem6  15204  rlim  15452  rlimclim1  15502  climsup  15627  caurcvg2  15635  caucvgb  15637  iseralt  15642  sumss  15681  fsum2dlem  15727  mptfzshft  15735  modfsummod  15752  o1fsum  15771  incexclem  15796  divrcnv  15812  flo1  15814  fprodrev  15937  fprod2dlem  15940  ruclem6  16197  moddvds  16227  dvdsaddre2b  16271  dvdsflip  16281  addmodlteqALT  16289  nn0o  16347  fldivndvdslt  16380  bitsf1ocnv  16408  bitsf1  16410  sadcaddlem  16421  bezoutlem2  16504  bezoutlem4  16506  lcmgcdlem  16570  prmind2  16649  isprm5  16672  isprm6  16679  prmdvdsncoprmbd  16692  cncongrprm  16694  hashdvds  16740  crth  16743  eulerthlem2  16747  prmdiveq  16751  hashgcdlem  16753  hashgcdeq  16755  iserodd  16801  pclem  16804  pcprendvds2  16807  pcexp  16825  pcneg  16840  pc2dvds  16845  pcmpt  16858  prmpwdvds  16870  pockthg  16872  prmreclem5  16886  4sqlem11  16921  ramub2  16980  ramubcl  16984  ram0  16988  ramub1lem2  16993  ramcl  16995  prmgaplem3  17019  prmgaplem6  17022  setscom  17145  sscpwex  17777  initoeu2  17978  setcinv  18052  funcestrcsetclem9  18109  funcsetcestrclem9  18124  fullsetcestrc  18127  1stfcl  18158  2ndfcl  18159  hofpropd  18228  isacs3lem  18503  isacs4lem  18505  acsmap2d  18516  chnflenfi  18589  subsubmgm  18673  submnd0  18726  mndpsuppss  18728  subsubm  18779  insubm  18781  frmdup1  18827  frmdup3lem  18829  sgrp2nmndlem2  18890  isgrpinv  18964  subsubg  19120  cycsubgcl  19176  conjghm  19219  qusghm  19225  gsumwrev  19336  gsmsymgrfixlem1  19397  symgfixelsi  19405  symgsssg  19437  symgfisg  19438  psgnunilem2  19465  odf1o2  19543  sylow1lem1  19568  odcau  19574  pgpfi  19575  pgpssslw  19584  fislw  19595  efgtlen  19696  efginvrel2  19697  efgrelexlemb  19720  efgredeu  19722  efgcpbllemb  19725  frgpup1  19745  lt6abl  19865  gsum2d  19942  gsum2d2lem  19943  gsum2d2  19944  telgsumfzslem  19958  dmdprdsplit2lem  20017  ablfacrp  20038  pgpfac1lem3  20049  gsummgp0  20292  irredrmul  20402  subsubrng  20539  subsubrg  20574  rngcinv  20613  ringcinv  20647  fldhmsubc  20761  islss4  20956  lspextmo  21050  lspsnat  21142  prmirredlem  21451  znf1o  21530  znidomb  21540  frgpcyg  21552  psgnghm  21559  psgndiflemB  21579  frlmlbs  21776  frlmup1  21777  lindfind  21795  islindf3  21805  lindfmm  21806  issubassa3  21845  resspsradd  21953  resspsrmul  21954  psdmul  22158  coe1tmmul2  22266  pf1ind  22345  mamulid  22428  mat1dimelbas  22458  mdetdiaglem  22585  mdetralt2  22596  mndifsplit  22623  smadiadetglem2  22659  1elcpmat  22702  pmatcollpw3lem  22770  chfacfisf  22841  chfacfisfcpmat  22842  chfacffsupp  22843  chfacfscmulfsupp  22846  chfacfscmulgsum  22847  chfacfpmmulfsupp  22850  chfacfpmmulgsum  22851  chfacfpmmulgsum2  22852  cayhamlem1  22853  cpmadugsumlemF  22863  cayleyhamilton1  22879  tgcl  22956  pptbas  22995  clsval2  23037  mretopd  23079  lmbr2  23246  cncls2  23260  nrmsep  23344  regsep2  23363  cmpsublem  23386  cmpsub  23387  tgcmp  23388  uncmp  23390  hauscmplem  23393  iunconnlem  23414  1stcrest  23440  2ndcctbss  23442  2ndcsep  23446  dis2ndc  23447  hausllycmp  23481  dislly  23484  kgentopon  23525  1stckgen  23541  kgencn3  23545  ptpjpre1  23558  ptbasin  23564  ptpjopn  23599  dfac14  23605  ptcnplem  23608  txcn  23613  txindis  23621  txdis1cn  23622  ptrescn  23626  txcmplem1  23628  txcmp  23630  txhaus  23634  txlm  23635  tx1stc  23637  txkgen  23639  xkococn  23647  qtopcn  23701  kqreglem1  23728  kqreglem2  23729  kqnrmlem1  23730  kqnrmlem2  23731  hmeoimaf1o  23757  reghmph  23780  nrmhmph  23781  txhmeo  23790  ptuncnv  23794  filconn  23870  fbasrn  23871  fmfnfmlem2  23942  flimfnfcls  24015  cnpfcfi  24027  alexsublem  24031  alexsubALTlem2  24035  alexsubALTlem3  24036  alexsubALTlem4  24037  alexsubALT  24038  ptcmplem3  24041  cnextfval  24049  tsmsxp  24142  imasdsf1olem  24360  bl2in  24387  blssps  24411  blss  24412  blssexps  24413  blssex  24414  blcld  24492  stdbdxmet  24502  met1stc  24508  prdsxmslem2  24516  metcnp3  24527  metcnpi3  24533  txmetcnp  24534  nmo0  24722  nmoid  24729  icccmplem1  24810  icccmp  24813  xrge0tsms  24822  metdseq0  24842  cnheiborlem  24943  cnheibor  24944  cnllycmp  24945  pcoval2  25005  cmetcaulem  25277  iscmet3lem1  25280  iscmet3lem2  25281  equivcau  25289  lmcau  25302  cncmet  25311  ivthlem2  25441  ivthlem3  25442  ovoliunlem2  25492  ovolscalem2  25503  uniioombl  25578  dyaddisj  25585  opnmbllem  25590  volivth  25596  ismbfd  25628  ismbf3d  25643  mbfimaopnlem  25644  mbfinf  25654  itg1addlem4  25688  mbfi1fseqlem1  25704  mbfi1fseqlem3  25706  mbfi1fseqlem4  25707  mbfi1fseqlem5  25708  mbfi1fseqlem6  25709  itg2seq  25731  itg2lea  25733  itg2split  25738  itg2cnlem1  25750  bddiblnc  25831  limciun  25883  dvmptfsum  25964  rolle  25979  c1lip1  25986  dvcnvrelem1  26006  dvcnvre  26008  dvcvx  26009  itgsubst  26038  tdeglem4  26047  mdegmullem  26065  plyco0  26179  coemullem  26237  dgreq0  26252  dgrmul  26257  dgrco  26262  elqaalem2  26308  aannenlem1  26316  aaliou3lem9  26338  ulmres  26375  ulmshftlem  26376  angneg  26789  dcubic  26832  cxploglim  26963  cxploglim2  26964  scvxcvx  26971  lgamgulmlem5  27018  lgamcvg2  27040  ftalem2  27059  basellem3  27068  basellem4  27069  sqff1o  27167  fsumdvdsdiaglem  27168  dvdsflsumcom  27173  mpodvdsmulf1o  27179  dvdsmulf1o  27181  fsumvma2  27199  logfac2  27202  logfacrlim  27209  logexprlim  27210  dchrelbasd  27224  lgsne0  27320  lgsqrlem2  27332  lgsqrmodndvds  27338  gausslemma2dlem1a  27350  lgseisenlem2  27361  lgsquadlem1  27365  lgsquadlem2  27366  lgsquadlem3  27367  lgsquad2lem2  27370  2sqlem8  27411  2sqlem11  27414  2sqreultlem  27432  2sqreunnltlem  27435  chpo1ubb  27466  vmadivsum  27467  rplogsumlem2  27470  rpvmasumlem  27472  dchrmusum2  27479  dchrvmasumlem1  27480  dchrisum0fno1  27496  dchrisum0re  27498  dchrisum0lem1  27501  dchrisum0lem2  27503  dchrisum0lem3  27504  dchrisum0  27505  mulogsumlem  27516  mulog2sumlem2  27520  vmalogdivsum2  27523  logsqvma  27527  log2sumbnd  27529  selberglem3  27532  selberg  27533  selberg2lem  27535  selberg2b  27537  selberg3lem2  27543  pntrmax  27549  pntrsumo1  27550  pntlemn  27585  pntlemp  27595  qabvle  27610  ostthlem1  27612  ostthlem2  27613  ostth2lem2  27619  ostth3  27623  ltsres  27648  nosupno  27689  nosupbnd2  27702  noinfno  27704  noinfbnd2  27717  etaslts  27807  cuteq1  27831  addsproplem2  27984  mulsval  28123  precsexlem11  28231  n0fincut  28369  zmulscld  28411  bdayfinbndlem1  28481  idmot  28627  brbtwn2  28996  colinearalglem4  29000  colinearalg  29001  ax5seglem9  29028  axpaschlem  29031  axcontlem2  29056  axcontlem7  29061  axcontlem8  29062  eengtrkg  29077  upgr1eopALT  29208  uspgredg2vlem  29314  subumgr  29379  nbgr0edglem  29447  edgnbusgreu  29458  nb3grprlem1  29471  wlkl1loop  29728  pthdivtx  29817  usgr2pth  29854  crctcshwlkn0  29911  wlklnwwlkln1  29958  wwlksnext  29983  clwwlkccatlem  30081  clwlkclwwlklem2a  30090  clwwlkinwwlk  30132  clwwlkn1loopb  30135  clwwlkf  30139  wwlksext2clwwlk  30149  wwlksubclwwlk  30150  clwwlknscsh  30154  clwwlknon1  30189  clwwlknonex2e  30202  1conngr  30286  n4cyclfrgr  30383  numclwwlk2lem1lem  30434  2clwwlk2clwwlk  30442  numclwwlk1lem2f1  30449  numclwlk1lem1  30461  numclwwlk2lem1  30468  numclwlk2lem2f  30469  numclwwlk7  30483  frgrogt3nreg  30489  grpoidinvlem1  30597  grpoidinvlem3  30599  grporcan  30611  nmlnoubi  30889  blocnilem  30897  ipblnfi  30948  htthlem  31010  ocsh  31376  shmodsi  31482  pjhthlem2  31485  5oalem2  31748  eigposi  31929  nmopub2tALT  32002  nmfnleub2  32019  nmcexi  32119  nmopcoi  32188  kbass3  32211  mdslmd1lem1  32418  mdslmd1lem2  32419  chirredlem2  32484  chirredlem4  32486  mdsymlem3  32498  mdsymlem5  32500  sumdmdii  32508  sumdmdlem  32511  sumdmdlem2  32512  foresf1o  32596  disjxpin  32681  1stpreimas  32802  resf1o  32826  nn0xmulclb  32867  wrdt2ind  33036  xrge0tsmsd  33158  gsumvsca1  33311  gsumvsca2  33312  islinds5  33454  1arithidomlem2  33631  mplvrpmmhm  33742  irngnzply1  33887  mdetpmtr1  34019  mdetpmtr2  34020  pstmxmet  34093  qqhghm  34184  qqhrhm  34185  esumpcvgval  34274  volmeas  34427  imambfm  34458  dya2iocnrect  34477  oddpwdc  34550  sseqf  34588  orvcgteel  34664  orvclteel  34669  ballotlemsf1o  34710  bnj1110  35179  bnj1118  35181  f1resveqaeq  35281  txpconn  35475  connpconn  35478  cnllysconn  35488  rellysconn  35494  cvmsss2  35517  cvmlift2lem9  35554  satf00  35617  fmlasuc  35629  mrsubfval  35751  mppsval  35815  dfon2lem6  36029  wzel  36065  ifscgr  36287  cgrxfr  36298  btwnconn1lem5  36334  btwnconn1lem6  36335  btwnconn1lem12  36341  brsegle  36351  finminlem  36561  nn0prpwlem  36565  fnessref  36600  refssfne  36601  neibastop1  36602  topjoin  36608  fnemeet2  36610  weiunse  36711  mh-inf3f1  36784  bj-prmoore  37488  bj-finsumval0  37660  topdifinffinlem  37724  lindsadd  37995  matunitlindflem2  37999  poimirlem28  38030  poimirlem32  38034  opnmbllem0  38038  mblfinlem1  38039  mblfinlem4  38042  ismblfin  38043  mbfresfi  38048  itg2addnclem  38053  itg2addnclem3  38055  itg2addnc  38056  unirep  38096  frinfm  38117  sdclem2  38124  geomcau  38141  istotbnd3  38153  sstotbnd2  38156  sstotbnd  38157  sstotbnd3  38158  totbndbnd  38171  cntotbnd  38178  ismtyres  38190  heibor1lem  38191  heiborlem1  38193  heiborlem8  38200  ismndo1  38255  isdivrngo  38332  unichnidl  38413  erimeq2  39145  cvlcvr1  39846  ishlat3N  39861  llnmlplnN  40046  islvol2aN  40099  4atlem4c  40108  4atlem4d  40109  isline2  40281  isline3  40283  linepsubclN  40458  lhpexle3lem  40518  lhpjat2  40528  cdlemd4  40708  cdleme0cq  40722  cdleme32fva  40944  cdleme32fvaw  40946  tendo0mul  41333  tendo0mulr  41334  diameetN  41563  dvhvaddcl  41602  dvhvaddcomN  41603  cdlemm10N  41625  dvadiaN  41635  djavalN  41642  dihvalcqat  41746  dihopelvalcpre  41755  djhval  41905  dihjat1lem  41935  sticksstones11  42656  sticksstones22  42668  remul01  42899  zaddcom  42969  zmulcom  42973  fidomncyc  43036  evlselvlem  43053  evlselv  43054  fsuppind  43055  mhpind  43059  prjspertr  43070  prjsprellsp  43076  elrfi  43158  nacsfix  43176  fzsplit1nn0  43218  eldioph2  43226  lzenom  43234  irrapxlem3  43284  pellexlem5  43293  pell1234qrne0  43313  pell1234qrmulcl  43315  pell14qrdich  43329  pell1qrge1  43330  pellqrex  43339  reglogltb  43351  reglogleb  43352  rmxypairf1o  43371  rmxycomplete  43377  monotoddzzfi  43402  congadd  43426  congsym  43428  acongrep  43440  jm2.19lem3  43451  jm2.19lem4  43452  jm2.22  43455  jm2.25  43459  expdiophlem1  43481  wepwsolem  43502  kelac1  43523  lmhmfgsplit  43546  pwslnm  43554  hbtlem6  43589  hbt  43590  mon1psubm  43659  deg1mhm  43660  omord2lim  43760  succlg  43788  onmcl  43791  ofoafo  43816  ofoacom  43821  fzunt  43914  fzuntd  43915  fzunt1d  43916  fzuntgd  43917  iunrelexp0  44161  dssmapnvod  44479  gsumws3  44655  gsumws4  44656  mulltgt0  45485  fnchoice  45492  disjrnmpt2  45649  fzisoeu  45762  fsumiunss  46034  climinf  46065  mullimc  46075  mullimcf  46082  stoweidlem14  46471  stoweidlem17  46474  stoweidlem34  46491  stoweidlem50  46507  fourierdlem42  46606  fourierdlem62  46625  fourierdlem71  46634  fourierdlem76  46639  qndenserrnbllem  46751  subsaliuncl  46815  sge0resplit  46863  3f1oss1  47552  2reu8i  47590  addmodne  47827  fundcmpsurinjpreimafv  47897  iccpartigtl  47912  prproropf1olem2  47993  prproropf1olem4  47995  paireqne  48000  prmdvdsfmtnof1lem2  48077  nprmdvdsfacm1  48116  bgoldbtbndlem3  48312  bgoldbtbnd  48314  grimcnv  48393  gricushgr  48422  cycldlenngric  48433  grimedg  48440  grtrimap  48453  isubgr3stgrlem6  48476  isubgr3stgrlem7  48477  isubgr3stgrlem8  48478  isubgr3stgrlem9  48479  grlimfn  48484  gpgedg2iv  48572  gpg5nbgrvtx03starlem2  48574  gpg5nbgrvtx13starlem2  48577  uspgrsprf1  48652  isassintop  48715  2zlidl  48745  2zrngnmrid  48761  rngcinvALTV  48781  funcringcsetcALTV2lem9  48803  ringcinvALTV  48815  funcringcsetclem9ALTV  48826  fldhmsubcALTV  48838  gsumlsscl  48885  lincsum  48934  lindslinindsimp1  48962  lindslinindimp2lem4  48966  lincresunitlem2  48981  elfzolborelfzop1  49024  elbigo2  49057  digexp  49112  dig1  49113  nn0sumshdiglemB  49125  1arymaptf1  49147  2arymaptf1  49158  itcoval1  49168  itcoval2  49169  itcoval3  49170  itcovalsucov  49173  ackvalsuc1mpt  49183  itschlc0xyqsol  49272  brab2dd  49332  dmrnxp  49341  xpco2  49361  initopropd  49747  termopropd  49748  zeroopropd  49749  prcofpropd  49883  thincciso  49957  indthinc  49966  indthincALT  49967  oduoppcciso  50070  lanpropd  50119  ranpropd  50120