Theorem ad2antrl 728

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 717	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  770  simprll  778  simprlr  779  simprl1  1219  simprl2  1220  simprl3  1221  disjxiun  5089  reusv2lem4  5340  axprlem5OLD  5369  fr2nr  5596  somin1  6082  tz7.7  6333  f1oprg  6809  soisores  7264  elovmporab1w  7596  elovmporab1  7597  sorpssi  7665  onint  7726  ordsucelsuc  7755  elxp5  7856  resf1extb  7867  f1oabexg  7875  wemoiso  7908  wemoiso2  7909  el2xptp0  7971  frxp2  8077  frxp3  8084  ressuppss  8116  fprlem1  8233  tz7.48lem  8363  oalimcl  8478  oeeui  8520  nnaordex2  8557  oaabs2  8567  omabs  8569  swoer  8656  ralxpmap  8823  pw2f1olem  8998  enfixsn  9003  mapxpen  9060  mapunen  9063  php  9121  unxpdomlem2  9146  unxpdomlem3  9147  isfinite2  9187  fodomfi  9201  domunfican  9211  fodomfiOLD  9220  fissuni  9247  fipreima  9248  indexfi  9250  fsuppsssupp  9271  marypha1lem  9323  marypha2  9329  supmo  9342  infmo  9387  oieu  9431  brwdom2  9465  ixpiunwdom  9482  cantnfval2  9565  cantnfle  9567  cantnflt  9568  cantnf  9589  wemapwe  9593  cnfcom  9596  frrlem15  9653  rankonidlem  9724  r1pwcl  9743  eldju2ndl  9820  eldju2ndr  9821  djuun  9822  infxpenlem  9907  infxpenc2lem1  9913  fseqenlem1  9918  dfac8clem  9926  mappwen  10006  dfac3  10015  dfac5  10023  dfac12lem3  10040  infunsdom  10107  coftr  10167  ssfin4  10204  domfin4  10205  fin23lem26  10219  fin23lem22  10221  fin23lem28  10234  fin23lem32  10238  fin23lem40  10245  isf32lem5  10251  compssiso  10268  isf34lem4  10271  isfin1-3  10280  fin1a2lem13  10306  hsmexlem2  10321  hsmexlem4  10323  zorn2lem1  10390  ttukeylem6  10408  iundom2g  10434  konigthlem  10462  pwcfsdom  10477  fpwwe2lem11  10535  fpwwe2  10537  pwfseqlem3  10554  winalim2  10590  r1wunlim  10631  inttsk  10668  inar1  10669  grur1  10714  nqereq  10829  ltexprlem7  10936  prlem936  10941  00id  11291  addlid  11299  ltord1  11646  divdiv1  11835  divdiv2  11836  conjmul  11841  ltdivmul  12000  ledivmul  12001  lt2mul2div  12003  ltdiv23  12016  lediv23  12017  lediv12a  12018  ledivp1  12027  negfi  12074  nn0nndivcl  12456  nn0ge0div  12545  peano2uz2  12564  peano5uzi  12565  eluzp1m1  12761  qbtwnre  13101  xralrple  13107  xleadd1a  13155  xmulge0  13186  xmulass  13189  xlemul1a  13190  iooshf  13329  divelunit  13397  eluzgtdifelfzo  13630  modadd1  13812  modmul1  13831  seqcl2  13927  seqfveq2  13931  seqid2  13955  seqhomo  13956  seqdistr  13960  mulexpz  14009  leexp2r  14081  expnlbnd2  14141  expmulnbnd  14142  hashmap  14342  hashfun  14344  hashbclem  14359  hashfacen  14361  hashf1lem2  14363  hashf1  14364  ccatsymb  14489  swrdwrdsymb  14569  swrdsb0eq  14570  ccatpfx  14607  swrdswrd  14611  wrdind  14628  wrd2ind  14629  swrdccatin1  14631  swrdccatin2  14635  pfxccatin12lem2  14637  pfxccatin12  14639  swrdccat  14641  repswswrd  14690  0csh0  14699  cshwidxmod  14709  2cshw  14719  cshweqrep  14727  relexp0g  14929  relexpsucnnr  14932  relexpindlem  14970  01sqrexlem1  15149  01sqrexlem6  15154  rlim  15402  rlimclim1  15452  climsup  15577  caurcvg2  15585  caucvgb  15587  iseralt  15592  sumss  15631  fsum2dlem  15677  mptfzshft  15685  modfsummod  15701  o1fsum  15720  incexclem  15743  divrcnv  15759  flo1  15761  fprodrev  15884  fprod2dlem  15887  ruclem6  16144  moddvds  16174  dvdsaddre2b  16218  dvdsflip  16228  addmodlteqALT  16236  nn0o  16294  fldivndvdslt  16327  bitsf1ocnv  16355  bitsf1  16357  sadcaddlem  16368  bezoutlem2  16451  bezoutlem4  16453  lcmgcdlem  16517  prmind2  16596  isprm5  16618  isprm6  16625  prmdvdsncoprmbd  16638  cncongrprm  16640  hashdvds  16686  crth  16689  eulerthlem2  16693  prmdiveq  16697  hashgcdlem  16699  hashgcdeq  16701  iserodd  16747  pclem  16750  pcprendvds2  16753  pcexp  16771  pcneg  16786  pc2dvds  16791  pcmpt  16804  prmpwdvds  16816  pockthg  16818  prmreclem5  16832  4sqlem11  16867  ramub2  16926  ramubcl  16930  ram0  16934  ramub1lem2  16939  ramcl  16941  prmgaplem3  16965  prmgaplem6  16968  setscom  17091  sscpwex  17722  initoeu2  17923  setcinv  17997  funcestrcsetclem9  18054  funcsetcestrclem9  18069  fullsetcestrc  18072  1stfcl  18103  2ndfcl  18104  hofpropd  18173  isacs3lem  18448  isacs4lem  18450  acsmap2d  18461  subsubmgm  18584  submnd0  18637  mndpsuppss  18639  subsubm  18690  insubm  18692  frmdup1  18738  frmdup3lem  18740  sgrp2nmndlem2  18798  isgrpinv  18872  subsubg  19028  cycsubgcl  19085  conjghm  19128  qusghm  19134  gsumwrev  19245  gsmsymgrfixlem1  19306  symgfixelsi  19314  symgsssg  19346  symgfisg  19347  psgnunilem2  19374  odf1o2  19452  sylow1lem1  19477  odcau  19483  pgpfi  19484  pgpssslw  19493  fislw  19504  efgtlen  19605  efginvrel2  19606  efgrelexlemb  19629  efgredeu  19631  efgcpbllemb  19634  frgpup1  19654  lt6abl  19774  gsum2d  19851  gsum2d2lem  19852  gsum2d2  19853  telgsumfzslem  19867  dmdprdsplit2lem  19926  ablfacrp  19947  pgpfac1lem3  19958  gsummgp0  20203  irredrmul  20312  subsubrng  20448  subsubrg  20483  rngcinv  20522  ringcinv  20556  fldhmsubc  20670  islss4  20865  lspextmo  20960  lspsnat  21052  prmirredlem  21379  znf1o  21458  znidomb  21468  frgpcyg  21480  psgnghm  21487  psgndiflemB  21507  frlmlbs  21704  frlmup1  21705  lindfind  21723  islindf3  21733  lindfmm  21734  issubassa3  21773  resspsradd  21882  resspsrmul  21883  psdmul  22051  coe1tmmul2  22160  pf1ind  22240  mamulid  22326  mat1dimelbas  22356  mdetdiaglem  22483  mdetralt2  22494  mndifsplit  22521  smadiadetglem2  22557  1elcpmat  22600  pmatcollpw3lem  22668  chfacfisf  22739  chfacfisfcpmat  22740  chfacffsupp  22741  chfacfscmulfsupp  22744  chfacfscmulgsum  22745  chfacfpmmulfsupp  22748  chfacfpmmulgsum  22749  chfacfpmmulgsum2  22750  cayhamlem1  22751  cpmadugsumlemF  22761  cayleyhamilton1  22777  tgcl  22854  pptbas  22893  clsval2  22935  mretopd  22977  lmbr2  23144  cncls2  23158  nrmsep  23242  regsep2  23261  cmpsublem  23284  cmpsub  23285  tgcmp  23286  uncmp  23288  hauscmplem  23291  iunconnlem  23312  1stcrest  23338  2ndcctbss  23340  2ndcsep  23344  dis2ndc  23345  hausllycmp  23379  dislly  23382  kgentopon  23423  1stckgen  23439  kgencn3  23443  ptpjpre1  23456  ptbasin  23462  ptpjopn  23497  dfac14  23503  ptcnplem  23506  txcn  23511  txindis  23519  txdis1cn  23520  ptrescn  23524  txcmplem1  23526  txcmp  23528  txhaus  23532  txlm  23533  tx1stc  23535  txkgen  23537  xkococn  23545  qtopcn  23599  kqreglem1  23626  kqreglem2  23627  kqnrmlem1  23628  kqnrmlem2  23629  hmeoimaf1o  23655  reghmph  23678  nrmhmph  23679  txhmeo  23688  ptuncnv  23692  filconn  23768  fbasrn  23769  fmfnfmlem2  23840  flimfnfcls  23913  cnpfcfi  23925  alexsublem  23929  alexsubALTlem2  23933  alexsubALTlem3  23934  alexsubALTlem4  23935  alexsubALT  23936  ptcmplem3  23939  cnextfval  23947  tsmsxp  24040  imasdsf1olem  24259  bl2in  24286  blssps  24310  blss  24311  blssexps  24312  blssex  24313  blcld  24391  stdbdxmet  24401  met1stc  24407  prdsxmslem2  24415  metcnp3  24426  metcnpi3  24432  txmetcnp  24433  nmo0  24621  nmoid  24628  icccmplem1  24709  icccmp  24712  xrge0tsms  24721  metdseq0  24741  cnheiborlem  24851  cnheibor  24852  cnllycmp  24853  pcoval2  24914  cmetcaulem  25186  iscmet3lem1  25189  iscmet3lem2  25190  equivcau  25198  lmcau  25211  cncmet  25220  ivthlem2  25351  ivthlem3  25352  ovoliunlem2  25402  ovolscalem2  25413  uniioombl  25488  dyaddisj  25495  opnmbllem  25500  volivth  25506  ismbfd  25538  ismbf3d  25553  mbfimaopnlem  25554  mbfinf  25564  itg1addlem4  25598  mbfi1fseqlem1  25614  mbfi1fseqlem3  25616  mbfi1fseqlem4  25617  mbfi1fseqlem5  25618  mbfi1fseqlem6  25619  itg2seq  25641  itg2lea  25643  itg2split  25648  itg2cnlem1  25660  bddiblnc  25741  limciun  25793  dvmptfsum  25877  rolle  25892  c1lip1  25900  dvcnvrelem1  25920  dvcnvre  25922  dvcvx  25923  itgsubst  25954  tdeglem4  25963  mdegmullem  25981  plyco0  26095  coemullem  26153  dgreq0  26169  dgrmul  26174  dgrco  26179  elqaalem2  26226  aannenlem1  26234  aaliou3lem9  26256  ulmres  26295  ulmshftlem  26296  angneg  26711  dcubic  26754  cxploglim  26886  cxploglim2  26887  scvxcvx  26894  lgamgulmlem5  26941  lgamcvg2  26963  ftalem2  26982  basellem3  26991  basellem4  26992  sqff1o  27090  fsumdvdsdiaglem  27091  dvdsflsumcom  27096  mpodvdsmulf1o  27102  dvdsmulf1o  27104  fsumvma2  27123  logfac2  27126  logfacrlim  27133  logexprlim  27134  dchrelbasd  27148  lgsne0  27244  lgsqrlem2  27256  lgsqrmodndvds  27262  gausslemma2dlem1a  27274  lgseisenlem2  27285  lgsquadlem1  27289  lgsquadlem2  27290  lgsquadlem3  27291  lgsquad2lem2  27294  2sqlem8  27335  2sqlem11  27338  2sqreultlem  27356  2sqreunnltlem  27359  chpo1ubb  27390  vmadivsum  27391  rplogsumlem2  27394  rpvmasumlem  27396  dchrmusum2  27403  dchrvmasumlem1  27404  dchrisum0fno1  27420  dchrisum0re  27422  dchrisum0lem1  27425  dchrisum0lem2  27427  dchrisum0lem3  27428  dchrisum0  27429  mulogsumlem  27440  mulog2sumlem2  27444  vmalogdivsum2  27447  logsqvma  27451  log2sumbnd  27453  selberglem3  27456  selberg  27457  selberg2lem  27459  selberg2b  27461  selberg3lem2  27467  pntrmax  27473  pntrsumo1  27474  pntlemn  27509  pntlemp  27519  qabvle  27534  ostthlem1  27536  ostthlem2  27537  ostth2lem2  27543  ostth3  27547  sltres  27572  nosupno  27613  nosupbnd2  27626  noinfno  27628  noinfbnd2  27641  etasslt  27724  cuteq1  27748  addsproplem2  27882  mulsval  28017  precsexlem11  28124  n0sfincut  28251  zmulscld  28290  idmot  28482  brbtwn2  28850  colinearalglem4  28854  colinearalg  28855  ax5seglem9  28882  axpaschlem  28885  axcontlem2  28910  axcontlem7  28915  axcontlem8  28916  eengtrkg  28931  upgr1eopALT  29062  uspgredg2vlem  29168  subumgr  29233  nbgr0edglem  29301  edgnbusgreu  29312  nb3grprlem1  29325  wlkl1loop  29583  pthdivtx  29672  usgr2pth  29709  crctcshwlkn0  29766  wlklnwwlkln1  29813  wwlksnext  29838  clwwlkccatlem  29933  clwlkclwwlklem2a  29942  clwwlkinwwlk  29984  clwwlkn1loopb  29987  clwwlkf  29991  wwlksext2clwwlk  30001  wwlksubclwwlk  30002  clwwlknscsh  30006  clwwlknon1  30041  clwwlknonex2e  30054  1conngr  30138  n4cyclfrgr  30235  numclwwlk2lem1lem  30286  2clwwlk2clwwlk  30294  numclwwlk1lem2f1  30301  numclwlk1lem1  30313  numclwwlk2lem1  30320  numclwlk2lem2f  30321  numclwwlk7  30335  frgrogt3nreg  30341  grpoidinvlem1  30448  grpoidinvlem3  30450  grporcan  30462  nmlnoubi  30740  blocnilem  30748  ipblnfi  30799  htthlem  30861  ocsh  31227  shmodsi  31333  pjhthlem2  31336  5oalem2  31599  eigposi  31780  nmopub2tALT  31853  nmfnleub2  31870  nmcexi  31970  nmopcoi  32039  kbass3  32062  mdslmd1lem1  32269  mdslmd1lem2  32270  chirredlem2  32335  chirredlem4  32337  mdsymlem3  32349  mdsymlem5  32351  sumdmdii  32359  sumdmdlem  32362  sumdmdlem2  32363  foresf1o  32448  disjxpin  32532  1stpreimas  32649  resf1o  32674  nn0xmulclb  32715  wrdt2ind  32896  xrge0tsmsd  33016  gsumvsca1  33169  gsumvsca2  33170  islinds5  33305  1arithidomlem2  33474  mplvrpmmhm  33549  irngnzply1  33664  mdetpmtr1  33796  mdetpmtr2  33797  pstmxmet  33870  qqhghm  33961  qqhrhm  33962  esumpcvgval  34051  volmeas  34204  imambfm  34236  dya2iocnrect  34255  oddpwdc  34328  sseqf  34366  orvcgteel  34442  orvclteel  34447  ballotlemsf1o  34488  bnj1110  34955  bnj1118  34957  f1resveqaeq  35058  txpconn  35215  connpconn  35218  cnllysconn  35228  rellysconn  35234  cvmsss2  35257  cvmlift2lem9  35294  satf00  35357  fmlasuc  35369  mrsubfval  35491  mppsval  35555  dfon2lem6  35772  wzel  35808  ifscgr  36028  cgrxfr  36039  btwnconn1lem5  36075  btwnconn1lem6  36076  btwnconn1lem12  36082  brsegle  36092  finminlem  36302  nn0prpwlem  36306  fnessref  36341  refssfne  36342  neibastop1  36343  topjoin  36349  fnemeet2  36351  weiunse  36452  bj-prmoore  37099  bj-finsumval0  37269  topdifinffinlem  37331  lindsadd  37603  matunitlindflem2  37607  poimirlem28  37638  poimirlem32  37642  opnmbllem0  37646  mblfinlem1  37647  mblfinlem4  37650  ismblfin  37651  mbfresfi  37656  itg2addnclem  37661  itg2addnclem3  37663  itg2addnc  37664  unirep  37704  frinfm  37725  sdclem2  37732  geomcau  37749  istotbnd3  37761  sstotbnd2  37764  sstotbnd  37765  sstotbnd3  37766  totbndbnd  37779  cntotbnd  37786  ismtyres  37798  heibor1lem  37799  heiborlem1  37801  heiborlem8  37808  ismndo1  37863  isdivrngo  37940  unichnidl  38021  erimeq2  38666  cvlcvr1  39328  ishlat3N  39343  llnmlplnN  39528  islvol2aN  39581  4atlem4c  39590  4atlem4d  39591  isline2  39763  isline3  39765  linepsubclN  39940  lhpexle3lem  40000  lhpjat2  40010  cdlemd4  40190  cdleme0cq  40204  cdleme32fva  40426  cdleme32fvaw  40428  tendo0mul  40815  tendo0mulr  40816  diameetN  41045  dvhvaddcl  41084  dvhvaddcomN  41085  cdlemm10N  41107  dvadiaN  41117  djavalN  41124  dihvalcqat  41228  dihopelvalcpre  41237  djhval  41387  dihjat1lem  41417  sticksstones11  42139  sticksstones22  42151  f1o2d2  42216  remul01  42390  zaddcom  42447  zmulcom  42451  fidomncyc  42518  evlselvlem  42569  evlselv  42570  fsuppind  42573  mhpind  42577  prjspertr  42588  prjsprellsp  42594  elrfi  42677  nacsfix  42695  fzsplit1nn0  42737  eldioph2  42745  lzenom  42753  irrapxlem3  42807  pellexlem5  42816  pell1234qrne0  42836  pell1234qrmulcl  42838  pell14qrdich  42852  pell1qrge1  42853  pellqrex  42862  reglogltb  42874  reglogleb  42875  rmxypairf1o  42894  rmxycomplete  42900  monotoddzzfi  42925  congadd  42949  congsym  42951  acongrep  42963  jm2.19lem3  42974  jm2.19lem4  42975  jm2.22  42978  jm2.25  42982  expdiophlem1  43004  wepwsolem  43025  kelac1  43046  lmhmfgsplit  43069  pwslnm  43077  hbtlem6  43112  hbt  43113  mon1psubm  43182  deg1mhm  43183  omord2lim  43283  succlg  43311  onmcl  43314  ofoafo  43339  ofoacom  43344  fzunt  43438  fzuntd  43439  fzunt1d  43440  fzuntgd  43441  iunrelexp0  43685  dssmapnvod  44003  gsumws3  44179  gsumws4  44180  mulltgt0  45010  fnchoice  45017  disjrnmpt2  45176  fzisoeu  45292  fsumiunss  45566  climinf  45597  mullimc  45607  mullimcf  45614  stoweidlem14  46005  stoweidlem17  46008  stoweidlem34  46025  stoweidlem50  46041  fourierdlem42  46140  fourierdlem62  46159  fourierdlem71  46168  fourierdlem76  46173  qndenserrnbllem  46285  subsaliuncl  46349  sge0resplit  46397  upwrdfi  46878  3f1oss1  47069  2reu8i  47107  addmodne  47338  fundcmpsurinjpreimafv  47402  iccpartigtl  47417  prproropf1olem2  47498  prproropf1olem4  47500  paireqne  47505  prmdvdsfmtnof1lem2  47579  bgoldbtbndlem3  47801  bgoldbtbnd  47803  grimcnv  47882  gricushgr  47911  cycldlenngric  47922  grimedg  47929  grtrimap  47942  isubgr3stgrlem6  47965  isubgr3stgrlem7  47966  isubgr3stgrlem8  47967  isubgr3stgrlem9  47968  grlimfn  47973  gpgedg2iv  48061  gpg5nbgrvtx03starlem2  48063  gpg5nbgrvtx13starlem2  48066  uspgrsprf1  48141  isassintop  48204  2zlidl  48234  2zrngnmrid  48250  rngcinvALTV  48270  funcringcsetcALTV2lem9  48292  ringcinvALTV  48304  funcringcsetclem9ALTV  48315  fldhmsubcALTV  48327  gsumlsscl  48374  lincsum  48424  lindslinindsimp1  48452  lindslinindimp2lem4  48456  lincresunitlem2  48471  elfzolborelfzop1  48514  elbigo2  48547  digexp  48602  dig1  48603  nn0sumshdiglemB  48615  1arymaptf1  48637  2arymaptf1  48648  itcoval1  48658  itcoval2  48659  itcoval3  48660  itcovalsucov  48663  ackvalsuc1mpt  48673  itschlc0xyqsol  48762  brab2dd  48822  dmrnxp  48831  xpco2  48851  initopropd  49238  termopropd  49239  zeroopropd  49240  prcofpropd  49374  thincciso  49448  indthinc  49457  indthincALT  49458  oduoppcciso  49561  lanpropd  49610  ranpropd  49611