Theorem ad2antrl 729

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 481	. 2 ⊢ ((𝜒 ∧ 𝜑) → 𝜓)
3	2	adantrr 718	1 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜃)) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  simprl  771  simprll  779  simprlr  780  simprl1  1220  simprl2  1221  simprl3  1222  disjxiun  5082  reusv2lem4  5343  axprlem5OLD  5373  fr2nr  5608  somin1  6096  tz7.7  6349  f1oprg  6826  soisores  7282  elovmporab1w  7614  elovmporab1  7615  sorpssi  7683  onint  7744  ordsucelsuc  7773  elxp5  7874  resf1extb  7885  f1oabexg  7893  wemoiso  7926  wemoiso2  7927  el2xptp0  7989  frxp2  8094  frxp3  8101  ressuppss  8133  fprlem1  8250  tz7.48lem  8380  oalimcl  8495  oeeui  8538  nnaordex2  8575  oaabs2  8585  omabs  8587  swoer  8675  ralxpmap  8844  pw2f1olem  9019  enfixsn  9024  mapxpen  9081  mapunen  9084  php  9141  unxpdomlem2  9167  unxpdomlem3  9168  isfinite2  9208  fodomfi  9222  domunfican  9232  fodomfiOLD  9240  fissuni  9267  fipreima  9268  indexfi  9270  fsuppsssupp  9294  marypha1lem  9346  marypha2  9352  supmo  9365  infmo  9410  oieu  9454  brwdom2  9488  ixpiunwdom  9505  cantnfval2  9590  cantnfle  9592  cantnflt  9593  cantnf  9614  wemapwe  9618  cnfcom  9621  frrlem15  9681  rankonidlem  9752  r1pwcl  9771  eldju2ndl  9848  eldju2ndr  9849  djuun  9850  infxpenlem  9935  infxpenc2lem1  9941  fseqenlem1  9946  dfac8clem  9954  mappwen  10034  dfac3  10043  dfac5  10051  dfac12lem3  10068  infunsdom  10135  coftr  10195  ssfin4  10232  domfin4  10233  fin23lem26  10247  fin23lem22  10249  fin23lem28  10262  fin23lem32  10266  fin23lem40  10273  isf32lem5  10279  compssiso  10296  isf34lem4  10299  isfin1-3  10308  fin1a2lem13  10334  hsmexlem2  10349  hsmexlem4  10351  zorn2lem1  10418  ttukeylem6  10436  iundom2g  10462  konigthlem  10491  pwcfsdom  10506  fpwwe2lem11  10564  fpwwe2  10566  pwfseqlem3  10583  winalim2  10619  r1wunlim  10660  inttsk  10697  inar1  10698  grur1  10743  nqereq  10858  ltexprlem7  10965  prlem936  10970  00id  11321  addlid  11329  ltord1  11676  divdiv1  11866  divdiv2  11867  conjmul  11872  ltdivmul  12031  ledivmul  12032  lt2mul2div  12034  ltdiv23  12047  lediv23  12048  lediv12a  12049  ledivp1  12058  negfi  12105  nn0nndivcl  12509  nn0ge0div  12598  peano2uz2  12617  peano5uzi  12618  eluzp1m1  12814  qbtwnre  13151  xralrple  13157  xleadd1a  13205  xmulge0  13236  xmulass  13239  xlemul1a  13240  iooshf  13379  divelunit  13447  eluzgtdifelfzo  13682  modadd1  13867  modmul1  13886  seqcl2  13982  seqfveq2  13986  seqid2  14010  seqhomo  14011  seqdistr  14015  mulexpz  14064  leexp2r  14136  expnlbnd2  14196  expmulnbnd  14197  hashmap  14397  hashfun  14399  hashbclem  14414  hashfacen  14416  hashf1lem2  14418  hashf1  14419  ccatsymb  14545  swrdwrdsymb  14625  swrdsb0eq  14626  ccatpfx  14663  swrdswrd  14667  wrdind  14684  wrd2ind  14685  swrdccatin1  14687  swrdccatin2  14691  pfxccatin12lem2  14693  pfxccatin12  14695  swrdccat  14697  repswswrd  14746  0csh0  14755  cshwidxmod  14765  2cshw  14775  cshweqrep  14783  relexp0g  14984  relexpsucnnr  14987  relexpindlem  15025  01sqrexlem1  15204  01sqrexlem6  15209  rlim  15457  rlimclim1  15507  climsup  15632  caurcvg2  15640  caucvgb  15642  iseralt  15647  sumss  15686  fsum2dlem  15732  mptfzshft  15740  modfsummod  15757  o1fsum  15776  incexclem  15801  divrcnv  15817  flo1  15819  fprodrev  15942  fprod2dlem  15945  ruclem6  16202  moddvds  16232  dvdsaddre2b  16276  dvdsflip  16286  addmodlteqALT  16294  nn0o  16352  fldivndvdslt  16385  bitsf1ocnv  16413  bitsf1  16415  sadcaddlem  16426  bezoutlem2  16509  bezoutlem4  16511  lcmgcdlem  16575  prmind2  16654  isprm5  16677  isprm6  16684  prmdvdsncoprmbd  16697  cncongrprm  16699  hashdvds  16745  crth  16748  eulerthlem2  16752  prmdiveq  16756  hashgcdlem  16758  hashgcdeq  16760  iserodd  16806  pclem  16809  pcprendvds2  16812  pcexp  16830  pcneg  16845  pc2dvds  16850  pcmpt  16863  prmpwdvds  16875  pockthg  16877  prmreclem5  16891  4sqlem11  16926  ramub2  16985  ramubcl  16989  ram0  16993  ramub1lem2  16998  ramcl  17000  prmgaplem3  17024  prmgaplem6  17027  setscom  17150  sscpwex  17782  initoeu2  17983  setcinv  18057  funcestrcsetclem9  18114  funcsetcestrclem9  18129  fullsetcestrc  18132  1stfcl  18163  2ndfcl  18164  hofpropd  18233  isacs3lem  18508  isacs4lem  18510  acsmap2d  18521  chnflenfi  18594  subsubmgm  18678  submnd0  18731  mndpsuppss  18733  subsubm  18784  insubm  18786  frmdup1  18832  frmdup3lem  18834  sgrp2nmndlem2  18895  isgrpinv  18969  subsubg  19125  cycsubgcl  19181  conjghm  19224  qusghm  19230  gsumwrev  19341  gsmsymgrfixlem1  19402  symgfixelsi  19410  symgsssg  19442  symgfisg  19443  psgnunilem2  19470  odf1o2  19548  sylow1lem1  19573  odcau  19579  pgpfi  19580  pgpssslw  19589  fislw  19600  efgtlen  19701  efginvrel2  19702  efgrelexlemb  19725  efgredeu  19727  efgcpbllemb  19730  frgpup1  19750  lt6abl  19870  gsum2d  19947  gsum2d2lem  19948  gsum2d2  19949  telgsumfzslem  19963  dmdprdsplit2lem  20022  ablfacrp  20043  pgpfac1lem3  20054  gsummgp0  20297  irredrmul  20407  subsubrng  20540  subsubrg  20575  rngcinv  20614  ringcinv  20648  fldhmsubc  20762  islss4  20957  lspextmo  21051  lspsnat  21143  prmirredlem  21452  znf1o  21531  znidomb  21541  frgpcyg  21553  psgnghm  21560  psgndiflemB  21580  frlmlbs  21777  frlmup1  21778  lindfind  21796  islindf3  21806  lindfmm  21807  issubassa3  21846  resspsradd  21953  resspsrmul  21954  psdmul  22132  coe1tmmul2  22241  pf1ind  22320  mamulid  22406  mat1dimelbas  22436  mdetdiaglem  22563  mdetralt2  22574  mndifsplit  22601  smadiadetglem2  22637  1elcpmat  22680  pmatcollpw3lem  22748  chfacfisf  22819  chfacfisfcpmat  22820  chfacffsupp  22821  chfacfscmulfsupp  22824  chfacfscmulgsum  22825  chfacfpmmulfsupp  22828  chfacfpmmulgsum  22829  chfacfpmmulgsum2  22830  cayhamlem1  22831  cpmadugsumlemF  22841  cayleyhamilton1  22857  tgcl  22934  pptbas  22973  clsval2  23015  mretopd  23057  lmbr2  23224  cncls2  23238  nrmsep  23322  regsep2  23341  cmpsublem  23364  cmpsub  23365  tgcmp  23366  uncmp  23368  hauscmplem  23371  iunconnlem  23392  1stcrest  23418  2ndcctbss  23420  2ndcsep  23424  dis2ndc  23425  hausllycmp  23459  dislly  23462  kgentopon  23503  1stckgen  23519  kgencn3  23523  ptpjpre1  23536  ptbasin  23542  ptpjopn  23577  dfac14  23583  ptcnplem  23586  txcn  23591  txindis  23599  txdis1cn  23600  ptrescn  23604  txcmplem1  23606  txcmp  23608  txhaus  23612  txlm  23613  tx1stc  23615  txkgen  23617  xkococn  23625  qtopcn  23679  kqreglem1  23706  kqreglem2  23707  kqnrmlem1  23708  kqnrmlem2  23709  hmeoimaf1o  23735  reghmph  23758  nrmhmph  23759  txhmeo  23768  ptuncnv  23772  filconn  23848  fbasrn  23849  fmfnfmlem2  23920  flimfnfcls  23993  cnpfcfi  24005  alexsublem  24009  alexsubALTlem2  24013  alexsubALTlem3  24014  alexsubALTlem4  24015  alexsubALT  24016  ptcmplem3  24019  cnextfval  24027  tsmsxp  24120  imasdsf1olem  24338  bl2in  24365  blssps  24389  blss  24390  blssexps  24391  blssex  24392  blcld  24470  stdbdxmet  24480  met1stc  24486  prdsxmslem2  24494  metcnp3  24505  metcnpi3  24511  txmetcnp  24512  nmo0  24700  nmoid  24707  icccmplem1  24788  icccmp  24791  xrge0tsms  24800  metdseq0  24820  cnheiborlem  24921  cnheibor  24922  cnllycmp  24923  pcoval2  24983  cmetcaulem  25255  iscmet3lem1  25258  iscmet3lem2  25259  equivcau  25267  lmcau  25280  cncmet  25289  ivthlem2  25419  ivthlem3  25420  ovoliunlem2  25470  ovolscalem2  25481  uniioombl  25556  dyaddisj  25563  opnmbllem  25568  volivth  25574  ismbfd  25606  ismbf3d  25621  mbfimaopnlem  25622  mbfinf  25632  itg1addlem4  25666  mbfi1fseqlem1  25682  mbfi1fseqlem3  25684  mbfi1fseqlem4  25685  mbfi1fseqlem5  25686  mbfi1fseqlem6  25687  itg2seq  25709  itg2lea  25711  itg2split  25716  itg2cnlem1  25728  bddiblnc  25809  limciun  25861  dvmptfsum  25942  rolle  25957  c1lip1  25964  dvcnvrelem1  25984  dvcnvre  25986  dvcvx  25987  itgsubst  26016  tdeglem4  26025  mdegmullem  26043  plyco0  26157  coemullem  26215  dgreq0  26230  dgrmul  26235  dgrco  26240  elqaalem2  26286  aannenlem1  26294  aaliou3lem9  26316  ulmres  26353  ulmshftlem  26354  angneg  26767  dcubic  26810  cxploglim  26941  cxploglim2  26942  scvxcvx  26949  lgamgulmlem5  26996  lgamcvg2  27018  ftalem2  27037  basellem3  27046  basellem4  27047  sqff1o  27145  fsumdvdsdiaglem  27146  dvdsflsumcom  27151  mpodvdsmulf1o  27157  dvdsmulf1o  27159  fsumvma2  27177  logfac2  27180  logfacrlim  27187  logexprlim  27188  dchrelbasd  27202  lgsne0  27298  lgsqrlem2  27310  lgsqrmodndvds  27316  gausslemma2dlem1a  27328  lgseisenlem2  27339  lgsquadlem1  27343  lgsquadlem2  27344  lgsquadlem3  27345  lgsquad2lem2  27348  2sqlem8  27389  2sqlem11  27392  2sqreultlem  27410  2sqreunnltlem  27413  chpo1ubb  27444  vmadivsum  27445  rplogsumlem2  27448  rpvmasumlem  27450  dchrmusum2  27457  dchrvmasumlem1  27458  dchrisum0fno1  27474  dchrisum0re  27476  dchrisum0lem1  27479  dchrisum0lem2  27481  dchrisum0lem3  27482  dchrisum0  27483  mulogsumlem  27494  mulog2sumlem2  27498  vmalogdivsum2  27501  logsqvma  27505  log2sumbnd  27507  selberglem3  27510  selberg  27511  selberg2lem  27513  selberg2b  27515  selberg3lem2  27521  pntrmax  27527  pntrsumo1  27528  pntlemn  27563  pntlemp  27573  qabvle  27588  ostthlem1  27590  ostthlem2  27591  ostth2lem2  27597  ostth3  27601  ltsres  27626  nosupno  27667  nosupbnd2  27680  noinfno  27682  noinfbnd2  27695  etaslts  27785  cuteq1  27809  addsproplem2  27962  mulsval  28101  precsexlem11  28209  n0fincut  28347  zmulscld  28389  bdayfinbndlem1  28459  idmot  28605  brbtwn2  28974  colinearalglem4  28978  colinearalg  28979  ax5seglem9  29006  axpaschlem  29009  axcontlem2  29034  axcontlem7  29039  axcontlem8  29040  eengtrkg  29055  upgr1eopALT  29186  uspgredg2vlem  29292  subumgr  29357  nbgr0edglem  29425  edgnbusgreu  29436  nb3grprlem1  29449  wlkl1loop  29706  pthdivtx  29795  usgr2pth  29832  crctcshwlkn0  29889  wlklnwwlkln1  29936  wwlksnext  29961  clwwlkccatlem  30059  clwlkclwwlklem2a  30068  clwwlkinwwlk  30110  clwwlkn1loopb  30113  clwwlkf  30117  wwlksext2clwwlk  30127  wwlksubclwwlk  30128  clwwlknscsh  30132  clwwlknon1  30167  clwwlknonex2e  30180  1conngr  30264  n4cyclfrgr  30361  numclwwlk2lem1lem  30412  2clwwlk2clwwlk  30420  numclwwlk1lem2f1  30427  numclwlk1lem1  30439  numclwwlk2lem1  30446  numclwlk2lem2f  30447  numclwwlk7  30461  frgrogt3nreg  30467  grpoidinvlem1  30575  grpoidinvlem3  30577  grporcan  30589  nmlnoubi  30867  blocnilem  30875  ipblnfi  30926  htthlem  30988  ocsh  31354  shmodsi  31460  pjhthlem2  31463  5oalem2  31726  eigposi  31907  nmopub2tALT  31980  nmfnleub2  31997  nmcexi  32097  nmopcoi  32166  kbass3  32189  mdslmd1lem1  32396  mdslmd1lem2  32397  chirredlem2  32462  chirredlem4  32464  mdsymlem3  32476  mdsymlem5  32478  sumdmdii  32486  sumdmdlem  32489  sumdmdlem2  32490  foresf1o  32574  disjxpin  32658  1stpreimas  32779  resf1o  32803  nn0xmulclb  32844  wrdt2ind  33013  xrge0tsmsd  33134  gsumvsca1  33287  gsumvsca2  33288  islinds5  33427  1arithidomlem2  33596  mplvrpmmhm  33690  irngnzply1  33835  mdetpmtr1  33967  mdetpmtr2  33968  pstmxmet  34041  qqhghm  34132  qqhrhm  34133  esumpcvgval  34222  volmeas  34375  imambfm  34406  dya2iocnrect  34425  oddpwdc  34498  sseqf  34536  orvcgteel  34612  orvclteel  34617  ballotlemsf1o  34658  bnj1110  35124  bnj1118  35126  f1resveqaeq  35228  txpconn  35414  connpconn  35417  cnllysconn  35427  rellysconn  35433  cvmsss2  35456  cvmlift2lem9  35493  satf00  35556  fmlasuc  35568  mrsubfval  35690  mppsval  35754  dfon2lem6  35968  wzel  36004  ifscgr  36226  cgrxfr  36237  btwnconn1lem5  36273  btwnconn1lem6  36274  btwnconn1lem12  36280  brsegle  36290  finminlem  36500  nn0prpwlem  36504  fnessref  36539  refssfne  36540  neibastop1  36541  topjoin  36547  fnemeet2  36549  weiunse  36650  mh-inf3f1  36723  bj-prmoore  37427  bj-finsumval0  37599  topdifinffinlem  37663  lindsadd  37934  matunitlindflem2  37938  poimirlem28  37969  poimirlem32  37973  opnmbllem0  37977  mblfinlem1  37978  mblfinlem4  37981  ismblfin  37982  mbfresfi  37987  itg2addnclem  37992  itg2addnclem3  37994  itg2addnc  37995  unirep  38035  frinfm  38056  sdclem2  38063  geomcau  38080  istotbnd3  38092  sstotbnd2  38095  sstotbnd  38096  sstotbnd3  38097  totbndbnd  38110  cntotbnd  38117  ismtyres  38129  heibor1lem  38130  heiborlem1  38132  heiborlem8  38139  ismndo1  38194  isdivrngo  38271  unichnidl  38352  erimeq2  39084  cvlcvr1  39785  ishlat3N  39800  llnmlplnN  39985  islvol2aN  40038  4atlem4c  40047  4atlem4d  40048  isline2  40220  isline3  40222  linepsubclN  40397  lhpexle3lem  40457  lhpjat2  40467  cdlemd4  40647  cdleme0cq  40661  cdleme32fva  40883  cdleme32fvaw  40885  tendo0mul  41272  tendo0mulr  41273  diameetN  41502  dvhvaddcl  41541  dvhvaddcomN  41542  cdlemm10N  41564  dvadiaN  41574  djavalN  41581  dihvalcqat  41685  dihopelvalcpre  41694  djhval  41844  dihjat1lem  41874  sticksstones11  42595  sticksstones22  42607  f1o2d2  42674  remul01  42839  zaddcom  42909  zmulcom  42913  fidomncyc  42980  evlselvlem  43019  evlselv  43020  fsuppind  43023  mhpind  43027  prjspertr  43038  prjsprellsp  43044  elrfi  43126  nacsfix  43144  fzsplit1nn0  43186  eldioph2  43194  lzenom  43202  irrapxlem3  43252  pellexlem5  43261  pell1234qrne0  43281  pell1234qrmulcl  43283  pell14qrdich  43297  pell1qrge1  43298  pellqrex  43307  reglogltb  43319  reglogleb  43320  rmxypairf1o  43339  rmxycomplete  43345  monotoddzzfi  43370  congadd  43394  congsym  43396  acongrep  43408  jm2.19lem3  43419  jm2.19lem4  43420  jm2.22  43423  jm2.25  43427  expdiophlem1  43449  wepwsolem  43470  kelac1  43491  lmhmfgsplit  43514  pwslnm  43522  hbtlem6  43557  hbt  43558  mon1psubm  43627  deg1mhm  43628  omord2lim  43728  succlg  43756  onmcl  43759  ofoafo  43784  ofoacom  43789  fzunt  43882  fzuntd  43883  fzunt1d  43884  fzuntgd  43885  iunrelexp0  44129  dssmapnvod  44447  gsumws3  44623  gsumws4  44624  mulltgt0  45453  fnchoice  45460  disjrnmpt2  45618  fzisoeu  45733  fsumiunss  46005  climinf  46036  mullimc  46046  mullimcf  46053  stoweidlem14  46442  stoweidlem17  46445  stoweidlem34  46462  stoweidlem50  46478  fourierdlem42  46577  fourierdlem62  46596  fourierdlem71  46605  fourierdlem76  46610  qndenserrnbllem  46722  subsaliuncl  46786  sge0resplit  46834  3f1oss1  47523  2reu8i  47561  addmodne  47798  fundcmpsurinjpreimafv  47868  iccpartigtl  47883  prproropf1olem2  47964  prproropf1olem4  47966  paireqne  47971  prmdvdsfmtnof1lem2  48048  nprmdvdsfacm1  48087  bgoldbtbndlem3  48283  bgoldbtbnd  48285  grimcnv  48364  gricushgr  48393  cycldlenngric  48404  grimedg  48411  grtrimap  48424  isubgr3stgrlem6  48447  isubgr3stgrlem7  48448  isubgr3stgrlem8  48449  isubgr3stgrlem9  48450  grlimfn  48455  gpgedg2iv  48543  gpg5nbgrvtx03starlem2  48545  gpg5nbgrvtx13starlem2  48548  uspgrsprf1  48623  isassintop  48686  2zlidl  48716  2zrngnmrid  48732  rngcinvALTV  48752  funcringcsetcALTV2lem9  48774  ringcinvALTV  48786  funcringcsetclem9ALTV  48797  fldhmsubcALTV  48809  gsumlsscl  48856  lincsum  48905  lindslinindsimp1  48933  lindslinindimp2lem4  48937  lincresunitlem2  48952  elfzolborelfzop1  48995  elbigo2  49028  digexp  49083  dig1  49084  nn0sumshdiglemB  49096  1arymaptf1  49118  2arymaptf1  49129  itcoval1  49139  itcoval2  49140  itcoval3  49141  itcovalsucov  49144  ackvalsuc1mpt  49154  itschlc0xyqsol  49243  brab2dd  49303  dmrnxp  49312  xpco2  49332  initopropd  49718  termopropd  49719  zeroopropd  49720  prcofpropd  49854  thincciso  49928  indthinc  49937  indthincALT  49938  oduoppcciso  50041  lanpropd  50090  ranpropd  50091