Theorem ad2antrl 740

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  simprl  782  simprll  790  simprlr  791  simprl1  1235  simprl2  1236  simprl3  1237  disjxiun  5110  reusv2lem4  5373  axprlem5OLD  5403  fr2nr  5639  somin1  6134  tz7.7  6387  f1oprg  6868  soisores  7326  elovmporab1w  7658  elovmporab1  7659  sorpssi  7727  onint  7789  ordsucelsuc  7818  elxp5  7920  resf1extb  7931  f1oabexg  7938  wemoiso  7970  wemoiso2  7971  el2xptp0  8033  mpof1o2d  8121  frxp2  8140  frxp3  8147  ressuppss  8179  fprlem1  8297  tz7.48lem  8428  oalimcl  8545  oeeui  8588  nnaordex2  8625  oaabs2  8635  omabs  8637  swoer  8726  ralxpmap  8894  pw2f1olem  9069  enfixsn  9074  mapxpen  9131  mapunen  9134  php  9191  unxpdomlem2  9217  unxpdomlem3  9218  isfinite2  9258  fodomfi  9272  domunfican  9281  fissuni  9314  fipreima  9315  indexfi  9317  fsuppsssupp  9341  marypha1lem  9393  marypha2  9399  supmo  9412  infmo  9457  oieu  9501  brwdom2  9535  ixpiunwdom  9552  cantnfval2  9638  cantnfle  9640  cantnflt  9641  cantnf  9662  wemapwe  9666  cnfcom  9669  frrlem15  9729  rankonidlem  9800  r1pwcl  9819  eldju2ndl  9910  eldju2ndr  9911  djuun  9912  infxpenlem  9997  infxpenc2lem1  10003  fseqenlem1  10008  dfac8clem  10016  mappwen  10096  dfac3  10105  dfac5  10112  dfac12lem3  10129  infunsdom  10196  coftr  10257  ssfin4  10294  domfin4  10295  fin23lem26  10309  fin23lem22  10311  fin23lem28  10324  fin23lem32  10328  fin23lem40  10335  isf32lem5  10341  compssiso  10358  isf34lem4  10361  isfin1-3  10370  fin1a2lem13  10396  hsmexlem2  10411  hsmexlem4  10413  zorn2lem1  10480  ttukeylem6  10498  iundom2g  10524  konigthlem  10553  pwcfsdom  10568  fpwwe2lem11  10626  fpwwe2  10628  pwfseqlem3  10645  winalim2  10681  r1wunlim  10722  inttsk  10759  inar1  10760  grur1  10805  nqereq  10920  ltexprlem7  11027  prlem936  11032  00id  11385  addlid  11393  ltord1  11740  divdiv1  11926  divdiv2  11927  conjmul  11932  ltdivmul  12090  ledivmul  12091  lt2mul2div  12093  ltdiv23  12106  lediv23  12107  lediv12a  12108  ledivp1  12117  negfi  12164  nn0nndivcl  12576  nn0ge0div  12665  peano2uz2  12684  peano5uzi  12685  eluzp1m1  12888  qbtwnre  13225  xralrple  13231  xleadd1a  13279  xmulge0  13310  xmulass  13313  xlemul1a  13314  iooshf  13453  divelunit  13521  eluzgtdifelfzo  13756  modadd1  13941  modmul1  13960  seqcl2  14056  seqfveq2  14060  seqid2  14084  seqhomo  14085  seqdistr  14089  mulexpz  14138  leexp2r  14210  expnlbnd2  14270  expmulnbnd  14271  hashmap  14472  hashfun  14474  hashbclem  14489  hashfacen  14491  hashf1lem2  14493  hashf1  14494  ccatsymb  14620  swrdwrdsymb  14700  swrdsb0eq  14701  ccatpfx  14738  swrdswrd  14742  wrdind  14759  wrd2ind  14760  swrdccatin1  14762  swrdccatin2  14766  pfxccatin12lem2  14768  pfxccatin12  14770  swrdccat  14772  repswswrd  14821  0csh0  14830  cshwidxmod  14840  2cshw  14850  cshweqrep  14858  relexp0g  15059  relexpsucnnr  15062  relexpindlem  15100  01sqrexlem1  15293  01sqrexlem6  15298  rlim  15546  rlimclim1  15596  climsup  15721  caurcvg2  15729  caucvgb  15731  iseralt  15736  sumss  15775  fsum2dlem  15821  mptfzshft  15829  modfsummod  15846  o1fsum  15865  incexclem  15890  divrcnv  15906  flo1  15908  fprodrev  16031  fprod2dlem  16034  ruclem6  16291  moddvds  16321  dvdsaddre2b  16365  dvdsflip  16375  addmodlteqALT  16383  nn0o  16441  fldivndvdslt  16474  bitsf1ocnv  16502  bitsf1  16504  sadcaddlem  16515  bezoutlem2  16598  bezoutlem4  16600  lcmgcdlem  16664  prmind2  16743  isprm5  16766  isprm6  16773  prmdvdsncoprmbd  16786  cncongrprm  16788  hashdvds  16834  crth  16837  eulerthlem2  16841  prmdiveq  16845  hashgcdlem  16847  hashgcdeq  16849  iserodd  16895  pclem  16898  pcprendvds2  16901  pcexp  16919  pcneg  16934  pc2dvds  16939  pcmpt  16952  prmpwdvds  16964  pockthg  16966  prmreclem5  16980  4sqlem11  17015  ramub2  17074  ramubcl  17078  ram0  17082  ramub1lem2  17087  ramcl  17089  prmgaplem3  17113  prmgaplem6  17116  setscom  17240  sscpwex  17872  initoeu2  18073  setcinv  18147  funcestrcsetclem9  18204  funcsetcestrclem9  18219  fullsetcestrc  18222  1stfcl  18253  2ndfcl  18254  hofpropd  18323  isacs3lem  18598  isacs4lem  18600  acsmap2d  18611  chnflenfi  18684  subsubmgm  18768  submnd0  18821  mndpsuppss  18823  subsubm  18875  insubm  18877  frmdup1  18923  frmdup3lem  18925  sgrp2nmndlem2  18986  isgrpinv  19060  subsubg  19216  cycsubgcl  19277  conjghm  19319  qusghm  19325  gsumwrev  19436  gsmsymgrfixlem1  19497  symgfixelsi  19505  symgsssg  19537  symgfisg  19538  psgnunilem2  19565  odf1o2  19643  sylow1lem1  19668  odcau  19674  pgpfi  19675  pgpssslw  19684  fislw  19695  efgtlen  19796  efginvrel2  19797  efgrelexlemb  19820  efgredeu  19822  efgcpbllemb  19825  frgpup1  19845  lt6abl  19965  gsum2d  20042  gsum2d2lem  20043  gsum2d2  20044  telgsumfzslem  20058  dmdprdsplit2lem  20117  ablfacrp  20138  pgpfac1lem3  20149  gsummgp0  20399  irredrmul  20509  subsubrng  20648  subsubrg  20683  rngcinv  20722  ringcinv  20756  fldhmsubc  20866  islss4  21061  lspextmo  21155  lspsnat  21247  prmirredlem  21591  znf1o  21670  znidomb  21680  frgpcyg  21692  psgnghm  21699  psgndiflemB  21719  frlmlbs  21916  frlmup1  21917  lindfind  21935  islindf3  21945  lindfmm  21946  issubassa3  21985  resspsradd  22093  resspsrmul  22094  psdmul  22298  coe1tmmul2  22406  pf1ind  22484  mamulid  22567  mat1dimelbas  22597  mdetdiaglem  22724  mdetralt2  22735  mndifsplit  22762  smadiadetglem2  22798  1elcpmat  22841  pmatcollpw3lem  22909  chfacfisf  22980  chfacfisfcpmat  22981  chfacffsupp  22982  chfacfscmulfsupp  22985  chfacfscmulgsum  22986  chfacfpmmulfsupp  22989  chfacfpmmulgsum  22990  chfacfpmmulgsum2  22991  cayhamlem1  22992  cpmadugsumlemF  23002  cayleyhamilton1  23018  tgcl  23095  pptbas  23134  clsval2  23176  mretopd  23218  lmbr2  23385  cncls2  23399  nrmsep  23483  regsep2  23502  cmpsublem  23525  cmpsub  23526  tgcmp  23527  uncmp  23529  hauscmplem  23532  iunconnlem  23553  1stcrest  23579  2ndcctbss  23581  2ndcsep  23585  dis2ndc  23586  hausllycmp  23620  dislly  23623  kgentopon  23664  1stckgen  23680  kgencn3  23684  ptpjpre1  23697  ptbasin  23703  ptpjopn  23738  dfac14  23744  ptcnplem  23747  txcn  23752  txindis  23760  txdis1cn  23761  ptrescn  23765  txcmplem1  23767  txcmp  23769  txhaus  23773  txlm  23774  tx1stc  23776  txkgen  23778  xkococn  23786  qtopcn  23840  kqreglem1  23867  kqreglem2  23868  kqnrmlem1  23869  kqnrmlem2  23870  hmeoimaf1o  23896  reghmph  23919  nrmhmph  23920  txhmeo  23929  ptuncnv  23933  filconn  24009  fbasrn  24010  fmfnfmlem2  24081  flimfnfcls  24154  cnpfcfi  24166  alexsublem  24170  alexsubALTlem2  24174  alexsubALTlem3  24175  alexsubALTlem4  24176  alexsubALT  24177  ptcmplem3  24180  cnextfval  24188  tsmsxp  24281  imasdsf1olem  24499  bl2in  24526  blssps  24550  blss  24551  blssexps  24552  blssex  24553  blcld  24631  stdbdxmet  24641  met1stc  24647  prdsxmslem2  24655  metcnp3  24666  metcnpi3  24672  txmetcnp  24673  nmo0  24861  nmoid  24868  icccmplem1  24949  icccmp  24952  xrge0tsms  24961  metdseq0  24981  cnheiborlem  25082  cnheibor  25083  cnllycmp  25084  pcoval2  25144  cmetcaulem  25416  iscmet3lem1  25419  iscmet3lem2  25420  equivcau  25428  lmcau  25441  cncmet  25450  ivthlem2  25580  ivthlem3  25581  ovoliunlem2  25631  ovolscalem2  25642  uniioombl  25717  dyaddisj  25724  opnmbllem  25729  volivth  25735  ismbfd  25767  ismbf3d  25782  mbfimaopnlem  25783  mbfinf  25793  itg1addlem4  25827  mbfi1fseqlem1  25843  mbfi1fseqlem3  25845  mbfi1fseqlem4  25846  mbfi1fseqlem5  25847  mbfi1fseqlem6  25848  itg2seq  25870  itg2lea  25872  itg2split  25877  itg2cnlem1  25889  bddiblnc  25970  limciun  26022  dvmptfsum  26103  rolle  26118  c1lip1  26125  dvcnvrelem1  26145  dvcnvre  26147  dvcvx  26148  itgsubst  26177  tdeglem4  26186  mdegmullem  26204  plyco0  26318  coemullem  26376  dgreq0  26391  dgrmul  26396  dgrco  26401  elqaalem2  26450  aannenlem1  26458  aaliou3lem9  26480  ulmres  26517  ulmshftlem  26518  angneg  26934  dcubic  26977  cxploglim  27108  cxploglim2  27109  scvxcvx  27116  lgamgulmlem5  27163  lgamcvg2  27185  ftalem2  27204  basellem3  27213  basellem4  27214  sqff1o  27312  fsumdvdsdiaglem  27313  dvdsflsumcom  27318  mpodvdsmulf1o  27324  dvdsmulf1o  27326  fsumvma2  27344  logfac2  27347  logfacrlim  27354  logexprlim  27355  dchrelbasd  27369  lgsne0  27465  lgsqrlem2  27477  lgsqrmodndvds  27483  gausslemma2dlem1a  27495  lgseisenlem2  27506  lgsquadlem1  27510  lgsquadlem2  27511  lgsquadlem3  27512  lgsquad2lem2  27515  2sqlem8  27556  2sqlem11  27559  2sqreultlem  27577  2sqreunnltlem  27580  chpo1ubb  27611  vmadivsum  27612  rplogsumlem2  27615  rpvmasumlem  27617  dchrmusum2  27624  dchrvmasumlem1  27625  dchrisum0fno1  27641  dchrisum0re  27643  dchrisum0lem1  27646  dchrisum0lem2  27648  dchrisum0lem3  27649  dchrisum0  27650  mulogsumlem  27661  mulog2sumlem2  27665  vmalogdivsum2  27668  logsqvma  27672  log2sumbnd  27674  selberglem3  27677  selberg  27678  selberg2lem  27680  selberg2b  27682  selberg3lem2  27688  pntrmax  27694  pntrsumo1  27695  pntlemn  27730  pntlemp  27740  qabvle  27755  ostthlem1  27757  ostthlem2  27758  ostth2lem2  27764  ostth3  27768  ltsres  27792  nosupno  27833  nosupbnd2  27846  noinfno  27848  noinfbnd2  27861  etaslts  27952  cuteq1  27976  addsproplem2  28129  mulsval  28268  precsexlem11  28376  n0fincut  28514  zmulscld  28556  bdayfinbndlem1  28626  idmot  28772  plngval  29017  brbtwn2  29196  colinearalglem4  29200  colinearalg  29201  ax5seglem9  29228  axpaschlem  29231  axcontlem2  29256  axcontlem7  29261  axcontlem8  29262  eengtrkg  29277  upgr1eopALT  29408  uspgredg2vlem  29514  subumgr  29579  nbgr0edglem  29647  edgnbusgreu  29658  nb3grprlem1  29671  wlkl1loop  29928  pthdivtx  30017  usgr2pth  30054  crctcshwlkn0  30111  wlklnwwlkln1  30158  wwlksnext  30183  clwwlkccatlem  30281  clwlkclwwlklem2a  30290  clwwlkinwwlk  30332  clwwlkn1loopb  30335  clwwlkf  30339  wwlksext2clwwlk  30349  wwlksubclwwlk  30350  clwwlknscsh  30354  clwwlknon1  30389  clwwlknonex2e  30402  1conngr  30486  n4cyclfrgr  30583  numclwwlk2lem1lem  30634  2clwwlk2clwwlk  30642  numclwwlk1lem2f1  30649  numclwlk1lem1  30661  numclwwlk2lem1  30668  numclwlk2lem2f  30669  numclwwlk7  30683  frgrogt3nreg  30689  grpoidinvlem1  30797  grpoidinvlem3  30799  grporcan  30811  nmlnoubi  31089  blocnilem  31097  ipblnfi  31148  htthlem  31210  ocsh  31576  shmodsi  31682  pjhthlem2  31685  5oalem2  31948  eigposi  32129  nmopub2tALT  32202  nmfnleub2  32219  nmcexi  32319  nmopcoi  32388  kbass3  32411  mdslmd1lem1  32618  mdslmd1lem2  32619  chirredlem2  32684  chirredlem4  32686  mdsymlem3  32698  mdsymlem5  32700  sumdmdii  32708  sumdmdlem  32711  sumdmdlem2  32712  foresf1o  32791  disjxpin  32874  1stpreimas  32992  resf1o  33016  nn0xmulclb  33057  wrdt2ind  33214  xrge0tsmsd  33334  gsumvsca1  33487  gsumvsca2  33488  islinds5  33625  1arithidomlem2  33771  mplvrpmmhm  33881  irngnzply1  34026  mdetpmtr1  34158  mdetpmtr2  34159  pstmxmet  34232  qqhghm  34323  qqhrhm  34324  esumpcvgval  34413  volmeas  34566  imambfm  34597  dya2iocnrect  34616  oddpwdc  34689  sseqf  34727  orvcgteel  34803  orvclteel  34808  ballotlemsf1o  34849  bnj1110  35315  bnj1118  35317  f1resveqaeq  35417  txpconn  35657  connpconn  35660  cnllysconn  35670  rellysconn  35676  cvmsss2  35699  cvmlift2lem9  35736  satf00  35799  fmlasuc  35811  mrsubfval  35933  mppsval  35997  dfon2lem6  36211  wzel  36247  ifscgr  36469  cgrxfr  36480  btwnconn1lem5  36516  btwnconn1lem6  36517  btwnconn1lem12  36523  brsegle  36533  finminlem  36752  nn0prpwlem  36756  fnessref  36791  refssfne  36792  neibastop1  36793  topjoin  36799  fnemeet2  36801  weiunse  36902  mh-inf3f1  36975  bj-prmoore  37679  bj-finsumval0  37851  topdifinffinlem  37915  lindsadd  38186  matunitlindflem2  38190  poimirlem28  38221  poimirlem32  38225  opnmbllem0  38229  mblfinlem1  38230  mblfinlem4  38233  ismblfin  38234  mbfresfi  38239  itg2addnclem  38244  itg2addnclem3  38246  itg2addnc  38247  unirep  38287  frinfm  38308  sdclem2  38315  geomcau  38332  istotbnd3  38344  sstotbnd2  38347  sstotbnd  38348  sstotbnd3  38349  totbndbnd  38362  cntotbnd  38369  ismtyres  38381  heibor1lem  38382  heiborlem1  38384  heiborlem8  38391  ismndo1  38446  isdivrngo  38523  unichnidl  38604  erimeq2  39336  cvlcvr1  40037  ishlat3N  40052  llnmlplnN  40237  islvol2aN  40290  4atlem4c  40299  4atlem4d  40300  isline2  40472  isline3  40474  linepsubclN  40649  lhpexle3lem  40709  lhpjat2  40719  cdlemd4  40899  cdleme0cq  40913  cdleme32fva  41135  cdleme32fvaw  41137  tendo0mul  41524  tendo0mulr  41525  diameetN  41754  dvhvaddcl  41793  dvhvaddcomN  41794  cdlemm10N  41816  dvadiaN  41826  djavalN  41833  dihvalcqat  41937  dihopelvalcpre  41946  djhval  42096  dihjat1lem  42126  sticksstones11  42847  sticksstones22  42859  remul01  43092  zaddcom  43162  zmulcom  43166  fidomncyc  43229  evlselvlem  43246  evlselv  43247  fsuppind  43248  mhpind  43252  prjspertr  43263  prjsprellsp  43269  elrfi  43351  nacsfix  43369  fzsplit1nn0  43411  eldioph2  43419  lzenom  43427  irrapxlem3  43477  pellexlem5  43486  pell1234qrne0  43506  pell1234qrmulcl  43508  pell14qrdich  43522  pell1qrge1  43523  pellqrex  43532  reglogltb  43544  reglogleb  43545  rmxypairf1o  43564  rmxycomplete  43570  monotoddzzfi  43595  congadd  43619  congsym  43621  acongrep  43633  jm2.19lem3  43644  jm2.19lem4  43645  jm2.22  43648  jm2.25  43652  expdiophlem1  43674  wepwsolem  43695  kelac1  43716  lmhmfgsplit  43739  pwslnm  43747  hbtlem6  43782  hbt  43783  mon1psubm  43852  deg1mhm  43853  omord2lim  43953  succlg  43981  onmcl  43984  ofoafo  44009  ofoacom  44014  fzunt  44107  fzuntd  44108  fzunt1d  44109  fzuntgd  44110  iunrelexp0  44354  dssmapnvod  44672  gsumws3  44848  gsumws4  44849  mulltgt0  45668  fnchoice  45675  disjrnmpt2  45832  fzisoeu  45945  fsumiunss  46217  climinf  46248  mullimc  46258  mullimcf  46265  stoweidlem14  46654  stoweidlem17  46657  stoweidlem34  46674  stoweidlem50  46690  fourierdlem42  46789  fourierdlem62  46808  fourierdlem71  46817  fourierdlem76  46822  qndenserrnbllem  46934  subsaliuncl  46998  sge0resplit  47046  3f1oss1  47735  2reu8i  47773  addmodne  48010  fundcmpsurinjpreimafv  48080  iccpartigtl  48095  prproropf1olem2  48176  prproropf1olem4  48178  paireqne  48183  prmdvdsfmtnof1lem2  48260  nprmdvdsfacm1  48299  bgoldbtbndlem3  48495  bgoldbtbnd  48497  grimcnv  48576  gricushgr  48605  cycldlenngric  48616  grimedg  48623  grtrimap  48636  isubgr3stgrlem6  48659  isubgr3stgrlem7  48660  isubgr3stgrlem8  48661  isubgr3stgrlem9  48662  grlimfn  48667  gpgedg2iv  48755  gpg5nbgrvtx03starlem2  48757  gpg5nbgrvtx13starlem2  48760  uspgrsprf1  48835  isassintop  48898  2zlidl  48928  2zrngnmrid  48944  rngcinvALTV  48964  funcringcsetcALTV2lem9  48986  ringcinvALTV  48998  funcringcsetclem9ALTV  49009  fldhmsubcALTV  49021  gsumlsscl  49079  lincsum  49128  lindslinindsimp1  49156  lindslinindimp2lem4  49160  lincresunitlem2  49175  elfzolborelfzop1  49218  elbigo2  49251  digexp  49306  dig1  49307  nn0sumshdiglemB  49319  1arymaptf1  49341  2arymaptf1  49352  itcoval1  49362  itcoval2  49363  itcoval3  49364  itcovalsucov  49367  ackvalsuc1mpt  49377  itschlc0xyqsol  49466  brab2dd  49525  dmrnxp  49534  xpco2  49554  initopropd  49940  termopropd  49941  zeroopropd  49942  prcofpropd  50076  thincciso  50150  indthinc  50159  indthincALT  50160  oduoppcciso  50263  lanpropd  50312  ranpropd  50313