Theorem ad2antrl 741

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  simprl  783  simprll  791  simprlr  792  simprl1  1237  simprl2  1238  simprl3  1239  disjxiun  5100  reusv2lem4  5363  fr2nr  5628  somin1  6127  tz7.7  6388  f1oprg  6871  f1resveqaeq  7277  soisores  7335  elovmporab1w  7668  elovmporab1  7669  sorpssi  7745  onint  7804  ordsucelsuc  7833  elxp5  7935  resf1extb  7946  f1oabexg  7953  wemoiso  7985  wemoiso2  7986  el2xptp0  8047  mpof1o2d  8137  frxp2  8161  frxp3  8168  ressuppss  8200  fprlem1  8318  tz7.48lemOLD  8451  oalimcl  8568  oeeui  8611  nnaordex2  8648  oaabs2  8658  omabs  8660  swoer  8749  ralxpmap  8924  pw2f1olem  9100  enfixsn  9105  mapxpen  9162  mapunen  9165  php  9222  unxpdomlem2  9248  unxpdomlem3  9249  isfinite2  9290  fodomfi  9304  domunfican  9313  fissuni  9346  fipreima  9347  indexfi  9349  fsuppsssupp  9373  marypha1lem  9425  marypha2  9431  supmo  9444  infmo  9489  oieu  9533  brwdom2  9567  ixpiunwdom  9584  cantnfval2  9670  cantnfle  9672  cantnflt  9673  cantnf  9694  wemapwe  9698  cnfcom  9701  frrlem15  9761  rankonidlem  9838  r1pwcl  9861  eldju2ndl  10005  eldju2ndr  10006  djuun  10007  infxpenlem  10092  infxpenc2lem1  10098  fseqenlem1  10103  dfac8clem  10111  mappwen  10191  dfac3  10200  dfac5  10207  dfac12lem3  10224  infunsdom  10291  coftr  10351  ssfin4  10388  domfin4  10389  fin23lem26  10403  fin23lem22  10405  fin23lem28  10418  fin23lem32  10422  fin23lem40  10429  isf32lem5  10435  compssiso  10452  isf34lem4  10455  isfin1-3  10464  fin1a2lem13  10490  hsmexlem2  10505  hsmexlem4  10507  zorn2lem1  10574  ttukeylem6  10592  iundom2g  10624  konigthlem  10653  pwcfsdom  10668  fpwwe2lem11  10726  fpwwe2  10728  pwfseqlem3  10745  winalim2  10781  r1wunlim  10822  inttsk  10859  inar1  10860  grur1  10905  nqereq  11020  ltexprlem7  11127  prlem936  11132  00id  11485  addlid  11493  ltord1  11842  divdiv1  12028  divdiv2  12029  conjmul  12034  ltdivmul  12192  ledivmul  12193  lt2mul2div  12195  ltdiv23  12208  lediv23  12209  lediv12a  12210  ledivp1  12219  negfi  12266  nn0nndivcl  12678  nn0ge0div  12768  peano2uz2  12787  peano5uzi  12788  eluzp1m1  12991  qbtwnre  13329  xralrple  13335  xleadd1a  13383  xmulge0  13414  xmulass  13417  xlemul1a  13418  iooshf  13557  divelunit  13625  eluzgtdifelfzo  13862  modadd1  14048  modmul1  14067  seqcl2  14163  seqfveq2  14167  seqid2  14191  seqhomo  14192  seqdistr  14196  mulexpz  14245  leexp2r  14317  expnlbnd2  14378  expmulnbnd  14379  hashmap  14580  hashfun  14582  hashbclem  14597  hashfacen  14599  hashf1lem2  14601  hashf1  14602  ccatsymb  14728  swrdwrdsymb  14812  swrdsb0eq  14813  ccatpfx  14850  swrdswrd  14854  wrdind  14871  wrd2ind  14872  swrdccatin1  14874  swrdccatin2  14878  pfxccatin12lem2  14880  pfxccatin12  14882  swrdccat  14884  repswswrd  14935  0csh0  14944  cshwidxmod  14954  2cshw  14964  cshweqrep  14972  relexp0g  15175  relexpsucnnr  15178  relexpindlem  15216  01sqrexlem1  15409  01sqrexlem6  15414  rlim  15662  rlimclim1  15712  climsup  15837  caurcvg2  15845  caucvgb  15847  iseralt  15852  sumss  15890  fsum2dlem  15936  mptfzshft  15944  modfsummod  15961  o1fsum  15980  incexclem  16005  divrcnv  16021  flo1  16023  fprodrev  16144  fprod2dlem  16147  ruclem6  16403  moddvds  16433  dvdsaddre2b  16477  dvdsflip  16487  addmodlteqALT  16495  nn0o  16553  fldivndvdslt  16586  bitsf1ocnv  16614  bitsf1  16616  sadcaddlem  16627  bezoutlem2  16713  bezoutlem4  16715  lcmgcdlem  16781  prmind2  16860  isprm5  16883  isprm6  16890  prmdvdsncoprmbd  16903  cncongrprm  16905  hashdvds  16952  crth  16955  eulerthlem2  16959  prmdiveq  16963  hashgcdlem  16965  hashgcdeq  16967  iserodd  17013  pclem  17016  pcprendvds2  17019  pcexp  17037  pcneg  17052  pc2dvds  17057  pcmpt  17070  prmpwdvds  17082  pockthg  17084  prmreclem5  17098  4sqlem11  17133  ramub2  17192  ramubcl  17196  ram0  17200  ramub1lem2  17205  ramcl  17207  prmgaplem3  17231  prmgaplem6  17234  setscom  17358  sscpwex  17990  initoeu2  18191  setcinv  18265  funcestrcsetclem9  18322  funcsetcestrclem9  18337  fullsetcestrc  18340  1stfcl  18371  2ndfcl  18372  hofpropd  18441  isacs3lem  18716  isacs4lem  18718  acsmap2d  18729  chnflenfi  18802  subsubmgm  18899  submnd0OLD  18957  mndpsuppss  18959  subsubm  19012  insubm  19014  frmdup1  19060  frmdup3lem  19062  sgrp2nmndlem2  19123  isgrpinv  19204  subsubg  19360  cycsubgcl  19421  conjghm  19463  qusghm  19469  gsumwrev  19580  gsmsymgrfixlem1  19641  symgfixelsi  19649  symgsssg  19681  symgfisg  19682  psgnunilem2  19709  odf1o2  19787  sylow1lem1  19812  odcau  19818  pgpfi  19819  pgpssslw  19828  fislw  19839  efgtlen  19940  efginvrel2  19941  efgrelexlemb  19964  efgredeu  19966  efgcpbllemb  19969  frgpup1  19989  lt6abl  20109  gsum2d  20186  gsum2d2lem  20187  gsum2d2  20188  telgsumfzslem  20202  dmdprdsplit2lem  20261  ablfacrp  20282  pgpfac1lem3  20293  gsummgp0  20547  irredrmul  20657  subsubrng  20815  subsubrg  20850  rngcinv  20889  ringcinv  20923  fldhmsubc  21042  islss4  21237  lspextmo  21331  lspsnat  21423  prmirredlem  21778  znf1o  21857  znidomb  21867  frgpcyg  21879  psgnghm  21886  psgndiflemB  21906  frlmlbs  22103  frlmup1  22104  lindfind  22122  islindf3  22132  lindfmm  22133  issubassa3  22174  resspsradd  22282  resspsrmul  22283  psdmul  22487  coe1tmmul2  22595  pf1ind  22673  mamulid  22756  mat1dimelbas  22786  mdetdiaglem  22913  mdetralt2  22924  mndifsplit  22951  smadiadetglem2  22987  matunitlindflem2  22995  1elcpmat  23033  pmatcollpw3lem  23101  chfacfisf  23172  chfacfisfcpmat  23173  chfacffsupp  23174  chfacfscmulfsupp  23177  chfacfscmulgsum  23178  chfacfpmmulfsupp  23181  chfacfpmmulgsum  23182  chfacfpmmulgsum2  23183  cayhamlem1  23184  cpmadugsumlemF  23194  cayleyhamilton1  23210  tgcl  23287  pptbas  23326  clsval2  23368  mretopd  23410  lmbr2  23577  cncls2  23591  nrmsep  23675  regsep2  23694  cmpsublem  23717  cmpsub  23718  tgcmp  23719  uncmp  23721  hauscmplem  23724  iunconnlem  23745  1stcrest  23771  2ndcctbss  23774  2ndcsep  23778  dis2ndc  23779  hausllycmp  23813  dislly  23816  kgentopon  23857  1stckgen  23873  kgencn3  23877  ptpjpre1  23890  ptbasin  23896  ptpjopn  23931  dfac14  23937  ptcnplem  23940  txcn  23945  txindis  23953  txdis1cn  23954  ptrescn  23958  txcmplem1  23960  txcmp  23962  txhaus  23966  txlm  23967  tx1stc  23969  txkgen  23971  xkococn  23979  qtopcn  24033  kqreglem1  24060  kqreglem2  24061  kqnrmlem1  24062  kqnrmlem2  24063  hmeoimaf1o  24089  reghmph  24112  nrmhmph  24113  txhmeo  24122  ptuncnv  24126  filconn  24202  fbasrn  24203  fmfnfmlem2  24274  flimfnfcls  24347  cnpfcfi  24359  alexsublem  24363  alexsubALTlem2  24367  alexsubALTlem3  24368  alexsubALTlem4  24369  alexsubALT  24370  ptcmplem3  24373  cnextfval  24381  tsmsxp  24474  imasdsf1olem  24692  bl2in  24719  blssps  24743  blss  24744  blssexps  24745  blssex  24746  blcld  24824  stdbdxmet  24834  met1stc  24840  prdsxmslem2  24848  metcnp3  24859  metcnpi3  24865  txmetcnp  24866  nmo0  25054  nmoid  25061  icccmplem1  25142  icccmp  25145  xrge0tsms  25154  metdseq0  25174  cnheiborlem  25275  cnheibor  25276  cnllycmp  25277  pcoval2  25337  cmetcaulem  25609  iscmet3lem1  25612  iscmet3lem2  25613  equivcau  25621  lmcau  25634  cncmet  25643  ivthlem2  25773  ivthlem3  25774  ovoliunlem2  25824  ovolscalem2  25835  uniioombl  25910  dyaddisj  25917  opnmbllem  25922  volivth  25928  ismbfd  25960  ismbf3d  25975  mbfimaopnlem  25976  mbfinf  25986  itg1addlem4  26020  mbfi1fseqlem1  26036  mbfi1fseqlem3  26038  mbfi1fseqlem4  26039  mbfi1fseqlem5  26040  mbfi1fseqlem6  26041  itg2seq  26063  itg2lea  26065  itg2split  26070  itg2cnlem1  26082  bddiblnc  26162  limciun  26214  dvmptfsum  26295  rolle  26310  c1lip1  26317  dvcnvrelem1  26337  dvcnvre  26339  dvcvx  26340  itgsubst  26369  tdeglem4  26378  mdegmullem  26396  plyco0  26510  coemullem  26569  dgreq0  26584  dgrmul  26589  dgrco  26594  elqaalem2  26643  preimaaa  26646  aannenlem1  26655  aaliou3lem9  26677  ulmres  26715  ulmshftlem  26716  angneg  27131  dcubic  27174  cxploglim  27305  cxploglim2  27306  scvxcvx  27313  lgamgulmlem5  27360  lgamcvg2  27382  ftalem2  27401  basellem3  27410  basellem4  27411  sqff1o  27509  fsumdvdsdiaglem  27510  dvdsflsumcom  27515  mpodvdsmulf1o  27521  dvdsmulf1o  27523  fsumvma2  27541  logfac2  27544  logfacrlim  27551  logexprlim  27552  dchrelbasd  27566  lgsne0  27662  lgsqrlem2  27674  lgsqrmodndvds  27680  gausslemma2dlem1a  27692  lgseisenlem2  27703  lgsquadlem1  27707  lgsquadlem2  27708  lgsquadlem3  27709  lgsquad2lem2  27712  2sqlem8  27753  2sqlem11  27756  2sqreultlem  27774  2sqreunnltlem  27777  chpo1ubb  27808  vmadivsum  27809  rplogsumlem2  27812  rpvmasumlem  27814  dchrmusum2  27821  dchrvmasumlem1  27822  dchrisum0fno1  27838  dchrisum0re  27840  dchrisum0lem1  27843  dchrisum0lem2  27845  dchrisum0lem3  27846  dchrisum0  27847  mulogsumlem  27858  mulog2sumlem2  27862  vmalogdivsum2  27865  logsqvma  27869  log2sumbnd  27871  selberglem3  27874  selberg  27875  selberg2lem  27877  selberg2b  27879  selberg3lem2  27885  pntrmax  27891  pntrsumo1  27892  pntlemn  27927  pntlemp  27937  qabvle  27952  ostthlem1  27954  ostthlem2  27955  ostth2lem2  27961  ostth3  27965  ltsres  28019  nosupno  28060  nosupbnd2  28073  noinfno  28075  noinfbnd2  28088  etaslts  28179  cuteq1  28203  addsproplem2  28356  mulsval  28495  precsexlem11  28603  n0fincut  28741  zmulscld  28783  bdayfinbndlem1  28853  idmot  29000  plngval  29255  brbtwn2  29483  colinearalglem4  29487  colinearalg  29488  ax5seglem9  29515  axpaschlem  29518  axcontlem2  29543  axcontlem7  29548  axcontlem8  29549  eengtrkg  29564  upgr1eopALT  29695  uspgredg2vlem  29804  subumgr  29869  nbgr0edglem  29937  edgnbusgreu  29948  nb3grprlem1  29961  wlkl1loop  30218  pthdivtx  30312  usgr2pth  30350  crctcshwlkn0  30410  wlklnwwlkln1  30457  wwlksnext  30482  clwwlkccatlem  30580  clwlkclwwlklem2a  30589  clwwlkinwwlk  30631  clwwlkn1loopb  30634  clwwlkf  30638  wwlksext2clwwlk  30648  wwlksubclwwlk  30649  clwwlknscsh  30653  clwwlknon1  30688  clwwlknonex2e  30701  1conngr  30795  n4cyclfrgr  30892  numclwwlk2lem1lem  30943  2clwwlk2clwwlk  30951  numclwwlk1lem2f1  30958  numclwlk1lem1  30970  numclwwlk2lem1  30977  numclwlk2lem2f  30978  numclwwlk7  30992  frgrogt3nreg  30998  grpoidinvlem1  31106  grpoidinvlem3  31108  grporcan  31120  nmlnoubi  31398  blocnilem  31406  ipblnfi  31457  htthlem  31519  ocsh  31885  shmodsi  31991  pjhthlem2  31994  5oalem2  32257  eigposi  32438  nmopub2tALT  32511  nmfnleub2  32528  nmcexi  32628  nmopcoi  32697  kbass3  32720  mdslmd1lem1  32927  mdslmd1lem2  32928  chirredlem2  32993  chirredlem4  32995  mdsymlem3  33007  mdsymlem5  33009  sumdmdii  33017  sumdmdlem  33020  sumdmdlem2  33021  foresf1o  33100  disjxpin  33182  1stpreimas  33299  resf1o  33322  nn0xmulclb  33363  wrdt2ind  33516  xrge0tsmsd  33634  gsumvsca1  33787  gsumvsca2  33788  islinds5  33923  1arithidomlem2  34068  mplvrpmmhm  34178  irngnzply1  34323  mdetpmtr1  34455  mdetpmtr2  34456  pstmxmet  34529  qqhghm  34620  qqhrhm  34621  esumpcvgval  34710  volmeas  34864  imambfm  34894  dya2iocnrect  34913  oddpwdc  34986  sseqf  35024  orvcgteel  35100  orvclteel  35105  ballotlemsf1o  35146  bnj1110  35612  bnj1118  35614  txpconn  35997  connpconn  36000  cnllysconn  36010  rellysconn  36016  cvmsss2  36039  cvmlift2lem9  36076  satf00  36139  fmlasuc  36151  mrsubfval  36273  mppsval  36337  dfon2lem6  36550  wzel  36586  ifscgr  36809  cgrxfr  36820  btwnconn1lem5  36856  btwnconn1lem6  36857  btwnconn1lem12  36863  brsegle  36873  finminlem  37106  nn0prpwlem  37110  fnessref  37145  refssfne  37146  neibastop1  37147  topjoin  37153  fnemeet2  37155  weiunse  37256  bj-prmoore  38036  bj-finsumval0  38206  topdifinffinlem  38270  lindsadd  38536  poimirlem28  38566  poimirlem32  38570  opnmbllem0  38574  mblfinlem1  38575  mblfinlem4  38578  ismblfin  38579  mbfresfi  38584  itg2addnclem  38589  itg2addnclem3  38591  itg2addnc  38592  unirep  38648  frinfm  38669  sdclem2  38676  geomcau  38693  istotbnd3  38705  sstotbnd2  38708  sstotbnd  38709  sstotbnd3  38710  totbndbnd  38723  cntotbnd  38730  ismtyres  38742  heibor1lem  38743  heiborlem1  38745  heiborlem8  38752  ismndo1  38807  isdivrngo  38884  unichnidl  38965  erimeq2  39695  cvlcvr1  40396  ishlat3N  40411  llnmlplnN  40596  islvol2aN  40649  4atlem4c  40658  4atlem4d  40659  isline2  40831  isline3  40833  linepsubclN  41008  lhpexle3lem  41068  lhpjat2  41078  cdlemd4  41258  cdleme0cq  41272  cdleme32fva  41494  cdleme32fvaw  41496  tendo0mul  41883  tendo0mulr  41884  diameetN  42113  dvhvaddcl  42152  dvhvaddcomN  42153  cdlemm10N  42175  dvadiaN  42185  djavalN  42192  dihvalcqat  42296  dihopelvalcpre  42305  djhval  42455  dihjat1lem  42485  sticksstones11  43206  sticksstones22  43218  remul01  43458  zaddcom  43528  zmulcom  43532  fidomncyc  43599  evlselvlem  43616  evlselv  43617  fsuppind  43618  mhpind  43622  prjspertr  43633  prjsprellsp  43639  elrfi  43704  nacsfix  43722  fzsplit1nn0  43764  eldioph2  43772  lzenom  43780  irrapxlem3  43830  pellexlem5  43839  pell1234qrne0  43859  pell1234qrmulcl  43861  pell14qrdich  43875  pell1qrge1  43876  pellqrex  43885  reglogltb  43897  reglogleb  43898  rmxypairf1o  43917  rmxycomplete  43923  monotoddzzfi  43948  congadd  43972  congsym  43974  acongrep  43986  jm2.19lem3  43997  jm2.19lem4  43998  jm2.22  44001  jm2.25  44005  expdiophlem1  44027  wepwsolem  44048  kelac1  44064  lmhmfgsplit  44087  pwslnm  44095  hbtlem6  44130  hbt  44131  mon1psubm  44200  deg1mhm  44201  omord2lim  44301  succlg  44329  onmcl  44332  ofoafo  44357  ofoacom  44362  fzunt  44455  fzuntd  44456  fzunt1d  44457  fzuntgd  44458  iunrelexp0  44701  dssmapnvod  45019  gsumws3  45195  gsumws4  45196  mulltgt0  46038  fnchoice  46045  disjrnmpt2  46202  fzisoeu  46315  fsumiunss  46586  climinf  46617  mullimc  46627  mullimcf  46634  stoweidlem14  47023  stoweidlem17  47026  stoweidlem34  47043  stoweidlem50  47059  fourierdlem42  47158  fourierdlem62  47177  fourierdlem71  47186  fourierdlem76  47191  qndenserrnbllem  47303  subsaliuncl  47367  sge0resplit  47415  3f1oss1  48144  2reu8i  48182  addmodne  48419  fundcmpsurinjpreimafv  48489  iccpartigtl  48504  prproropf1olem2  48585  prproropf1olem4  48587  paireqne  48592  prmdvdsfmtnof1lem2  48669  nprmdvdsfacm1  48708  bgoldbtbndlem3  48904  bgoldbtbnd  48906  grimcnv  48985  gricushgr  49014  cycldlenngric  49025  grimedg  49032  grtrimap  49045  isubgr3stgrlem6  49068  isubgr3stgrlem7  49069  isubgr3stgrlem8  49070  isubgr3stgrlem9  49071  grlimfn  49076  gpgedg2iv  49164  gpg5nbgrvtx03starlem2  49166  gpg5nbgrvtx13starlem2  49169  uspgrsprf1  49244  isassintop  49306  2zlidl  49336  2zrngnmrid  49352  rngcinvALTV  49372  funcringcsetcALTV2lem9  49394  ringcinvALTV  49406  funcringcsetclem9ALTV  49417  fldhmsubcALTV  49429  gsumlsscl  49491  lincsum  49540  lindslinindsimp1  49568  lindslinindimp2lem4  49572  lincresunitlem2  49587  elfzolborelfzop1  49630  elbigo2  49663  digexp  49718  dig1  49719  nn0sumshdiglemB  49731  1arymaptf1  49753  2arymaptf1  49764  itcoval1  49774  itcoval2  49775  itcoval3  49776  itcovalsucov  49779  ackvalsuc1mpt  49789  itschlc0xyqsol  49878  brab2dd  49937  dmrnxp  49946  xpco2  49966  initopropd  50350  termopropd  50351  zeroopropd  50352  prcofpropd  50486  thincciso  50560  indthinc  50569  indthincALT  50570  oduoppcciso  50673  lanpropd  50722  ranpropd  50723