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  771  simprll  779  simprlr  780  simprl1  1217  simprl2  1218  simprl3  1219  disjxiun  5144  reusv2lem4  5406  axprlem5OLD  5435  fr2nr  5665  somin1  6155  tz7.7  6411  f1oprg  6893  soisores  7346  elovmporab1w  7679  elovmporab1  7680  sorpssi  7747  onint  7809  ordsucelsuc  7841  elxp5  7945  f1oabexg  7962  wemoiso  7996  wemoiso2  7997  el2xptp0  8059  frxp2  8167  frxp3  8174  ressuppss  8206  fprlem1  8323  tz7.48lem  8479  oalimcl  8596  oeeui  8638  nnaordex2  8675  oaabs2  8685  omabs  8687  swoer  8774  ralxpmap  8934  pw2f1olem  9114  enfixsn  9119  mapxpen  9181  mapunen  9184  php  9244  unxpdomlem2  9284  unxpdomlem3  9285  findcard3OLD  9316  isfinite2  9331  fodomfi  9347  domunfican  9358  fodomfiOLD  9367  fissuni  9394  fipreima  9395  indexfi  9397  fsuppsssupp  9418  marypha1lem  9470  marypha2  9476  supmo  9489  infmo  9532  oieu  9576  brwdom2  9610  ixpiunwdom  9627  cantnfval2  9706  cantnfle  9708  cantnflt  9709  cantnf  9730  wemapwe  9734  cnfcom  9737  frrlem15  9794  rankonidlem  9865  r1pwcl  9884  eldju2ndl  9961  eldju2ndr  9962  djuun  9963  infxpenlem  10050  infxpenc2lem1  10056  fseqenlem1  10061  dfac8clem  10069  mappwen  10149  dfac3  10158  dfac5  10166  dfac12lem3  10183  infunsdom  10250  coftr  10310  ssfin4  10347  domfin4  10348  fin23lem26  10362  fin23lem22  10364  fin23lem28  10377  fin23lem32  10381  fin23lem40  10388  isf32lem5  10394  compssiso  10411  isf34lem4  10414  isfin1-3  10423  fin1a2lem13  10449  hsmexlem2  10464  hsmexlem4  10466  zorn2lem1  10533  ttukeylem6  10551  iundom2g  10577  konigthlem  10605  pwcfsdom  10620  fpwwe2lem11  10678  fpwwe2  10680  pwfseqlem3  10697  winalim2  10733  r1wunlim  10774  inttsk  10811  inar1  10812  grur1  10857  nqereq  10972  ltexprlem7  11079  prlem936  11084  00id  11433  addlid  11441  ltord1  11786  divdiv1  11975  divdiv2  11976  conjmul  11981  ltdivmul  12140  ledivmul  12141  lt2mul2div  12143  ltdiv23  12156  lediv23  12157  lediv12a  12158  ledivp1  12167  negfi  12214  nn0nndivcl  12595  nn0ge0div  12684  peano2uz2  12703  peano5uzi  12704  eluzp1m1  12901  qbtwnre  13237  xralrple  13243  xleadd1a  13291  xmulge0  13322  xmulass  13325  xlemul1a  13326  iooshf  13462  divelunit  13530  eluzgtdifelfzo  13762  modadd1  13944  modmul1  13961  seqcl2  14057  seqfveq2  14061  seqid2  14085  seqhomo  14086  seqdistr  14090  mulexpz  14139  leexp2r  14210  expnlbnd2  14269  expmulnbnd  14270  hashmap  14470  hashfun  14472  hashbclem  14487  hashfacen  14489  hashf1lem2  14491  hashf1  14492  ccatsymb  14616  swrdwrdsymb  14696  swrdsb0eq  14697  ccatpfx  14735  swrdswrd  14739  wrdind  14756  wrd2ind  14757  swrdccatin1  14759  swrdccatin2  14763  pfxccatin12lem2  14765  pfxccatin12  14767  swrdccat  14769  repswswrd  14818  0csh0  14827  cshwidxmod  14837  2cshw  14847  cshweqrep  14855  relexp0g  15057  relexpsucnnr  15060  relexpindlem  15098  01sqrexlem1  15277  01sqrexlem6  15282  rlim  15527  rlimclim1  15577  climsup  15702  caurcvg2  15710  caucvgb  15712  iseralt  15717  sumss  15756  fsum2dlem  15802  mptfzshft  15810  modfsummod  15826  o1fsum  15845  incexclem  15868  divrcnv  15884  flo1  15886  fprodrev  16009  fprod2dlem  16012  ruclem6  16267  moddvds  16297  dvdsaddre2b  16340  dvdsflip  16350  addmodlteqALT  16358  nn0o  16416  fldivndvdslt  16449  bitsf1ocnv  16477  bitsf1  16479  sadcaddlem  16490  bezoutlem2  16573  bezoutlem4  16575  lcmgcdlem  16639  prmind2  16718  isprm5  16740  isprm6  16747  prmdvdsncoprmbd  16760  cncongrprm  16762  hashdvds  16808  crth  16811  eulerthlem2  16815  prmdiveq  16819  hashgcdlem  16821  hashgcdeq  16822  iserodd  16868  pclem  16871  pcprendvds2  16874  pcexp  16892  pcneg  16907  pc2dvds  16912  pcmpt  16925  prmpwdvds  16937  pockthg  16939  prmreclem5  16953  4sqlem11  16988  ramub2  17047  ramubcl  17051  ram0  17055  ramub1lem2  17060  ramcl  17062  prmgaplem3  17086  prmgaplem6  17089  setscom  17213  sscpwex  17862  initoeu2  18069  setcinv  18143  funcestrcsetclem9  18203  funcsetcestrclem9  18218  fullsetcestrc  18221  1stfcl  18252  2ndfcl  18253  hofpropd  18323  isacs3lem  18599  isacs4lem  18601  acsmap2d  18612  subsubmgm  18735  submnd0  18788  mndpsuppss  18790  subsubm  18841  insubm  18843  frmdup1  18889  frmdup3lem  18891  sgrp2nmndlem2  18949  isgrpinv  19023  subsubg  19179  cycsubgcl  19236  conjghm  19279  qusghm  19285  gsumwrev  19399  gsmsymgrfixlem1  19459  symgfixelsi  19467  symgsssg  19499  symgfisg  19500  psgnunilem2  19527  odf1o2  19605  sylow1lem1  19630  odcau  19636  pgpfi  19637  pgpssslw  19646  fislw  19657  efgtlen  19758  efginvrel2  19759  efgrelexlemb  19782  efgredeu  19784  efgcpbllemb  19787  frgpup1  19807  lt6abl  19927  gsum2d  20004  gsum2d2lem  20005  gsum2d2  20006  telgsumfzslem  20020  dmdprdsplit2lem  20079  ablfacrp  20100  pgpfac1lem3  20111  gsummgp0  20331  irredrmul  20443  subsubrng  20579  subsubrg  20614  rngcinv  20653  ringcinv  20687  fldhmsubc  20802  islss4  20977  lspextmo  21072  lspsnat  21164  prmirredlem  21500  znf1o  21587  znidomb  21597  frgpcyg  21609  psgnghm  21615  psgndiflemB  21635  frlmlbs  21834  frlmup1  21835  lindfind  21853  islindf3  21863  lindfmm  21864  issubassa3  21903  resspsradd  22012  resspsrmul  22013  psdmul  22187  coe1tmmul2  22294  pf1ind  22374  mamulid  22462  mat1dimelbas  22492  mdetdiaglem  22619  mdetralt2  22630  mndifsplit  22657  smadiadetglem2  22693  1elcpmat  22736  pmatcollpw3lem  22804  chfacfisf  22875  chfacfisfcpmat  22876  chfacffsupp  22877  chfacfscmulfsupp  22880  chfacfscmulgsum  22881  chfacfpmmulfsupp  22884  chfacfpmmulgsum  22885  chfacfpmmulgsum2  22886  cayhamlem1  22887  cpmadugsumlemF  22897  cayleyhamilton1  22913  tgcl  22991  pptbas  23030  clsval2  23073  mretopd  23115  lmbr2  23282  cncls2  23296  nrmsep  23380  regsep2  23399  cmpsublem  23422  cmpsub  23423  tgcmp  23424  uncmp  23426  hauscmplem  23429  iunconnlem  23450  1stcrest  23476  2ndcctbss  23478  2ndcsep  23482  dis2ndc  23483  hausllycmp  23517  dislly  23520  kgentopon  23561  1stckgen  23577  kgencn3  23581  ptpjpre1  23594  ptbasin  23600  ptpjopn  23635  dfac14  23641  ptcnplem  23644  txcn  23649  txindis  23657  txdis1cn  23658  ptrescn  23662  txcmplem1  23664  txcmp  23666  txhaus  23670  txlm  23671  tx1stc  23673  txkgen  23675  xkococn  23683  qtopcn  23737  kqreglem1  23764  kqreglem2  23765  kqnrmlem1  23766  kqnrmlem2  23767  hmeoimaf1o  23793  reghmph  23816  nrmhmph  23817  txhmeo  23826  ptuncnv  23830  filconn  23906  fbasrn  23907  fmfnfmlem2  23978  flimfnfcls  24051  cnpfcfi  24063  alexsublem  24067  alexsubALTlem2  24071  alexsubALTlem3  24072  alexsubALTlem4  24073  alexsubALT  24074  ptcmplem3  24077  cnextfval  24085  tsmsxp  24178  imasdsf1olem  24398  bl2in  24425  blssps  24449  blss  24450  blssexps  24451  blssex  24452  blcld  24533  stdbdxmet  24543  met1stc  24549  prdsxmslem2  24557  metcnp3  24568  metcnpi3  24574  txmetcnp  24575  nmo0  24771  nmoid  24778  icccmplem1  24857  icccmp  24860  xrge0tsms  24869  metdseq0  24889  cnheiborlem  24999  cnheibor  25000  cnllycmp  25001  pcoval2  25062  cmetcaulem  25335  iscmet3lem1  25338  iscmet3lem2  25339  equivcau  25347  lmcau  25360  cncmet  25369  ivthlem2  25500  ivthlem3  25501  ovoliunlem2  25551  ovolscalem2  25562  uniioombl  25637  dyaddisj  25644  opnmbllem  25649  volivth  25655  ismbfd  25687  ismbf3d  25702  mbfimaopnlem  25703  mbfinf  25713  itg1addlem4  25747  itg1addlem4OLD  25748  mbfi1fseqlem1  25764  mbfi1fseqlem3  25766  mbfi1fseqlem4  25767  mbfi1fseqlem5  25768  mbfi1fseqlem6  25769  itg2seq  25791  itg2lea  25793  itg2split  25798  itg2cnlem1  25810  bddiblnc  25891  limciun  25943  dvmptfsum  26027  rolle  26042  c1lip1  26050  dvcnvrelem1  26070  dvcnvre  26072  dvcvx  26073  itgsubst  26104  tdeglem4  26113  mdegmullem  26131  plyco0  26245  coemullem  26303  dgreq0  26319  dgrmul  26324  dgrco  26329  elqaalem2  26376  aannenlem1  26384  aaliou3lem9  26406  ulmres  26445  ulmshftlem  26446  angneg  26860  dcubic  26903  cxploglim  27035  cxploglim2  27036  scvxcvx  27043  lgamgulmlem5  27090  lgamcvg2  27112  ftalem2  27131  basellem3  27140  basellem4  27141  sqff1o  27239  fsumdvdsdiaglem  27240  dvdsflsumcom  27245  mpodvdsmulf1o  27251  dvdsmulf1o  27253  fsumvma2  27272  logfac2  27275  logfacrlim  27282  logexprlim  27283  dchrelbasd  27297  lgsne0  27393  lgsqrlem2  27405  lgsqrmodndvds  27411  gausslemma2dlem1a  27423  lgseisenlem2  27434  lgsquadlem1  27438  lgsquadlem2  27439  lgsquadlem3  27440  lgsquad2lem2  27443  2sqlem8  27484  2sqlem11  27487  2sqreultlem  27505  2sqreunnltlem  27508  chpo1ubb  27539  vmadivsum  27540  rplogsumlem2  27543  rpvmasumlem  27545  dchrmusum2  27552  dchrvmasumlem1  27553  dchrisum0fno1  27569  dchrisum0re  27571  dchrisum0lem1  27574  dchrisum0lem2  27576  dchrisum0lem3  27577  dchrisum0  27578  mulogsumlem  27589  mulog2sumlem2  27593  vmalogdivsum2  27596  logsqvma  27600  log2sumbnd  27602  selberglem3  27605  selberg  27606  selberg2lem  27608  selberg2b  27610  selberg3lem2  27616  pntrmax  27622  pntrsumo1  27623  pntlemn  27658  pntlemp  27668  qabvle  27683  ostthlem1  27685  ostthlem2  27686  ostth2lem2  27692  ostth3  27696  sltres  27721  nosupno  27762  nosupbnd2  27775  noinfno  27777  noinfbnd2  27790  etasslt  27872  cuteq1  27892  addsproplem2  28017  mulsval  28149  precsexlem11  28255  zmulscld  28397  idmot  28559  brbtwn2  28934  colinearalglem4  28938  colinearalg  28939  ax5seglem9  28966  axpaschlem  28969  axcontlem2  28994  axcontlem7  28999  axcontlem8  29000  eengtrkg  29015  upgr1eopALT  29148  uspgredg2vlem  29254  subumgr  29319  nbgr0edglem  29387  edgnbusgreu  29398  nb3grprlem1  29411  wlkl1loop  29670  pthdivtx  29761  usgr2pth  29796  crctcshwlkn0  29850  wlklnwwlkln1  29897  wwlksnext  29922  clwwlkccatlem  30017  clwlkclwwlklem2a  30026  clwwlkinwwlk  30068  clwwlkn1loopb  30071  clwwlkf  30075  wwlksext2clwwlk  30085  wwlksubclwwlk  30086  clwwlknscsh  30090  clwwlknon1  30125  clwwlknonex2e  30138  1conngr  30222  n4cyclfrgr  30319  numclwwlk2lem1lem  30370  2clwwlk2clwwlk  30378  numclwwlk1lem2f1  30385  numclwlk1lem1  30397  numclwwlk2lem1  30404  numclwlk2lem2f  30405  numclwwlk7  30419  frgrogt3nreg  30425  grpoidinvlem1  30532  grpoidinvlem3  30534  grporcan  30546  nmlnoubi  30824  blocnilem  30832  ipblnfi  30883  htthlem  30945  ocsh  31311  shmodsi  31417  pjhthlem2  31420  5oalem2  31683  eigposi  31864  nmopub2tALT  31937  nmfnleub2  31954  nmcexi  32054  nmopcoi  32123  kbass3  32146  mdslmd1lem1  32353  mdslmd1lem2  32354  chirredlem2  32419  chirredlem4  32421  mdsymlem3  32433  mdsymlem5  32435  sumdmdii  32443  sumdmdlem  32446  sumdmdlem2  32447  foresf1o  32531  disjxpin  32607  1stpreimas  32720  resf1o  32747  nn0xmulclb  32781  wrdt2ind  32922  xrge0tsmsd  33047  gsumvsca1  33214  gsumvsca2  33215  islinds5  33374  1arithidomlem2  33543  irngnzply1  33705  mdetpmtr1  33783  mdetpmtr2  33784  pstmxmet  33857  qqhghm  33950  qqhrhm  33951  esumpcvgval  34058  volmeas  34211  imambfm  34243  dya2iocnrect  34262  oddpwdc  34335  sseqf  34373  orvcgteel  34448  orvclteel  34453  ballotlemsf1o  34494  bnj1110  34974  bnj1118  34976  f1resveqaeq  35077  txpconn  35216  connpconn  35219  cnllysconn  35229  rellysconn  35235  cvmsss2  35258  cvmlift2lem9  35295  satf00  35358  fmlasuc  35370  mrsubfval  35492  mppsval  35556  dfon2lem6  35769  wzel  35805  ifscgr  36025  cgrxfr  36036  btwnconn1lem5  36072  btwnconn1lem6  36073  btwnconn1lem12  36079  brsegle  36089  finminlem  36300  nn0prpwlem  36304  fnessref  36339  refssfne  36340  neibastop1  36341  topjoin  36347  fnemeet2  36349  weiunse  36450  bj-prmoore  37097  bj-finsumval0  37267  topdifinffinlem  37329  lindsadd  37599  matunitlindflem2  37603  poimirlem28  37634  poimirlem32  37638  opnmbllem0  37642  mblfinlem1  37643  mblfinlem4  37646  ismblfin  37647  mbfresfi  37652  itg2addnclem  37657  itg2addnclem3  37659  itg2addnc  37660  unirep  37700  frinfm  37721  sdclem2  37728  geomcau  37745  istotbnd3  37757  sstotbnd2  37760  sstotbnd  37761  sstotbnd3  37762  totbndbnd  37775  cntotbnd  37782  ismtyres  37794  heibor1lem  37795  heiborlem1  37797  heiborlem8  37804  ismndo1  37859  isdivrngo  37936  unichnidl  38017  erimeq2  38659  cvlcvr1  39320  ishlat3N  39335  llnmlplnN  39521  islvol2aN  39574  4atlem4c  39583  4atlem4d  39584  isline2  39756  isline3  39758  linepsubclN  39933  lhpexle3lem  39993  lhpjat2  40003  cdlemd4  40183  cdleme0cq  40197  cdleme32fva  40419  cdleme32fvaw  40421  tendo0mul  40808  tendo0mulr  40809  diameetN  41038  dvhvaddcl  41077  dvhvaddcomN  41078  cdlemm10N  41100  dvadiaN  41110  djavalN  41117  dihvalcqat  41221  dihopelvalcpre  41230  djhval  41380  dihjat1lem  41410  sticksstones11  42137  sticksstones22  42149  metakunt15  42200  metakunt16  42201  f1o2d2  42252  remul01  42413  zaddcom  42458  zmulcom  42462  fidomncyc  42521  evlselvlem  42572  evlselv  42573  fsuppind  42576  mhpind  42580  prjspertr  42591  prjsprellsp  42597  elrfi  42681  nacsfix  42699  fzsplit1nn0  42741  eldioph2  42749  lzenom  42757  irrapxlem3  42811  pellexlem5  42820  pell1234qrne0  42840  pell1234qrmulcl  42842  pell14qrdich  42856  pell1qrge1  42857  pellqrex  42866  reglogltb  42878  reglogleb  42879  rmxypairf1o  42899  rmxycomplete  42905  monotoddzzfi  42930  congadd  42954  congsym  42956  acongrep  42968  jm2.19lem3  42979  jm2.19lem4  42980  jm2.22  42983  jm2.25  42987  expdiophlem1  43009  wepwsolem  43030  kelac1  43051  lmhmfgsplit  43074  pwslnm  43082  hbtlem6  43117  hbt  43118  mon1psubm  43187  deg1mhm  43188  omord2lim  43289  succlg  43317  onmcl  43320  ofoafo  43345  ofoacom  43350  fzunt  43444  fzuntd  43445  fzunt1d  43446  fzuntgd  43447  iunrelexp0  43691  dssmapnvod  44009  gsumws3  44185  gsumws4  44186  mulltgt0  44959  fnchoice  44966  disjrnmpt2  45130  fzisoeu  45250  fsumiunss  45530  climinf  45561  mullimc  45571  mullimcf  45578  stoweidlem14  45969  stoweidlem17  45972  stoweidlem34  45989  stoweidlem50  46005  fourierdlem42  46104  fourierdlem62  46123  fourierdlem71  46132  fourierdlem76  46137  qndenserrnbllem  46249  subsaliuncl  46313  sge0resplit  46361  upwrdfi  46840  3f1oss1  47024  2reu8i  47062  addmodne  47283  fundcmpsurinjpreimafv  47332  iccpartigtl  47347  prproropf1olem2  47428  prproropf1olem4  47430  paireqne  47435  prmdvdsfmtnof1lem2  47509  bgoldbtbndlem3  47731  bgoldbtbnd  47733  uspgrimprop  47810  grimcnv  47816  gricushgr  47823  grimedg  47840  grtrimap  47850  isubgr3stgrlem6  47873  isubgr3stgrlem7  47874  isubgr3stgrlem8  47875  isubgr3stgrlem9  47876  grlimfn  47881  gpg5nbgrvtx03starlem2  47959  gpg5nbgrvtx13starlem2  47962  uspgrsprf1  47990  isassintop  48053  2zlidl  48083  2zrngnmrid  48099  rngcinvALTV  48119  funcringcsetcALTV2lem9  48141  ringcinvALTV  48153  funcringcsetclem9ALTV  48164  fldhmsubcALTV  48176  gsumlsscl  48224  lincsum  48274  lindslinindsimp1  48302  lindslinindimp2lem4  48306  lincresunitlem2  48321  elfzolborelfzop1  48364  elbigo2  48401  digexp  48456  dig1  48457  nn0sumshdiglemB  48469  1arymaptf1  48491  2arymaptf1  48502  itcoval1  48512  itcoval2  48513  itcoval3  48514  itcovalsucov  48517  ackvalsuc1mpt  48527  itschlc0xyqsol  48616  thincciso  48848  indthinc  48852  indthincALT  48853  oduoppcciso  48881