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  5108  reusv2lem4  5374  axprlem5OLD  5404  fr2nr  5640  somin1  6135  tz7.7  6390  f1oprg  6871  f1resveqaeq  7276  soisores  7334  elovmporab1w  7667  elovmporab1  7668  sorpssi  7736  onint  7795  ordsucelsuc  7824  elxp5  7926  resf1extb  7937  f1oabexg  7944  wemoiso  7976  wemoiso2  7977  el2xptp0  8039  mpof1o2d  8127  frxp2  8146  frxp3  8153  ressuppss  8185  fprlem1  8303  tz7.48lem  8434  oalimcl  8551  oeeui  8594  nnaordex2  8631  oaabs2  8641  omabs  8643  swoer  8732  ralxpmap  8900  pw2f1olem  9076  enfixsn  9081  mapxpen  9138  mapunen  9141  php  9198  unxpdomlem2  9224  unxpdomlem3  9225  isfinite2  9265  fodomfi  9279  domunfican  9288  fissuni  9321  fipreima  9322  indexfi  9324  fsuppsssupp  9348  marypha1lem  9400  marypha2  9406  supmo  9419  infmo  9464  oieu  9508  brwdom2  9542  ixpiunwdom  9559  cantnfval2  9645  cantnfle  9647  cantnflt  9648  cantnf  9669  wemapwe  9673  cnfcom  9676  frrlem15  9736  rankonidlem  9807  r1pwcl  9826  eldju2ndl  9926  eldju2ndr  9927  djuun  9928  infxpenlem  10013  infxpenc2lem1  10019  fseqenlem1  10024  dfac8clem  10032  mappwen  10112  dfac3  10121  dfac5  10128  dfac12lem3  10145  infunsdom  10212  coftr  10272  ssfin4  10309  domfin4  10310  fin23lem26  10324  fin23lem22  10326  fin23lem28  10339  fin23lem32  10343  fin23lem40  10350  isf32lem5  10356  compssiso  10373  isf34lem4  10376  isfin1-3  10385  fin1a2lem13  10411  hsmexlem2  10426  hsmexlem4  10428  zorn2lem1  10495  ttukeylem6  10513  iundom2g  10543  konigthlem  10572  pwcfsdom  10587  fpwwe2lem11  10645  fpwwe2  10647  pwfseqlem3  10664  winalim2  10700  r1wunlim  10741  inttsk  10778  inar1  10779  grur1  10824  nqereq  10939  ltexprlem7  11046  prlem936  11051  00id  11404  addlid  11412  ltord1  11759  divdiv1  11945  divdiv2  11946  conjmul  11951  ltdivmul  12109  ledivmul  12110  lt2mul2div  12112  ltdiv23  12125  lediv23  12126  lediv12a  12127  ledivp1  12136  negfi  12183  nn0nndivcl  12595  nn0ge0div  12685  peano2uz2  12704  peano5uzi  12705  eluzp1m1  12908  qbtwnre  13245  xralrple  13251  xleadd1a  13299  xmulge0  13330  xmulass  13333  xlemul1a  13334  iooshf  13473  divelunit  13541  eluzgtdifelfzo  13777  modadd1  13963  modmul1  13982  seqcl2  14078  seqfveq2  14082  seqid2  14106  seqhomo  14107  seqdistr  14111  mulexpz  14160  leexp2r  14232  expnlbnd2  14292  expmulnbnd  14293  hashmap  14494  hashfun  14496  hashbclem  14511  hashfacen  14513  hashf1lem2  14515  hashf1  14516  ccatsymb  14642  swrdwrdsymb  14726  swrdsb0eq  14727  ccatpfx  14764  swrdswrd  14768  wrdind  14785  wrd2ind  14786  swrdccatin1  14788  swrdccatin2  14792  pfxccatin12lem2  14794  pfxccatin12  14796  swrdccat  14798  repswswrd  14849  0csh0  14858  cshwidxmod  14868  2cshw  14878  cshweqrep  14886  relexp0g  15087  relexpsucnnr  15090  relexpindlem  15128  01sqrexlem1  15321  01sqrexlem6  15326  rlim  15574  rlimclim1  15624  climsup  15749  caurcvg2  15757  caucvgb  15759  iseralt  15764  sumss  15802  fsum2dlem  15848  mptfzshft  15856  modfsummod  15873  o1fsum  15892  incexclem  15917  divrcnv  15933  flo1  15935  fprodrev  16058  fprod2dlem  16061  ruclem6  16317  moddvds  16347  dvdsaddre2b  16391  dvdsflip  16401  addmodlteqALT  16409  nn0o  16467  fldivndvdslt  16500  bitsf1ocnv  16528  bitsf1  16530  sadcaddlem  16541  bezoutlem2  16624  bezoutlem4  16626  lcmgcdlem  16690  prmind2  16769  isprm5  16792  isprm6  16799  prmdvdsncoprmbd  16812  cncongrprm  16814  hashdvds  16860  crth  16863  eulerthlem2  16867  prmdiveq  16871  hashgcdlem  16873  hashgcdeq  16875  iserodd  16921  pclem  16924  pcprendvds2  16927  pcexp  16945  pcneg  16960  pc2dvds  16965  pcmpt  16978  prmpwdvds  16990  pockthg  16992  prmreclem5  17006  4sqlem11  17041  ramub2  17100  ramubcl  17104  ram0  17108  ramub1lem2  17113  ramcl  17115  prmgaplem3  17139  prmgaplem6  17142  setscom  17266  sscpwex  17898  initoeu2  18099  setcinv  18173  funcestrcsetclem9  18230  funcsetcestrclem9  18245  fullsetcestrc  18248  1stfcl  18279  2ndfcl  18280  hofpropd  18349  isacs3lem  18624  isacs4lem  18626  acsmap2d  18637  chnflenfi  18710  subsubmgm  18804  submnd0OLD  18862  mndpsuppss  18864  subsubm  18916  insubm  18918  frmdup1  18964  frmdup3lem  18966  sgrp2nmndlem2  19027  isgrpinv  19108  subsubg  19264  cycsubgcl  19325  conjghm  19367  qusghm  19373  gsumwrev  19484  gsmsymgrfixlem1  19545  symgfixelsi  19553  symgsssg  19585  symgfisg  19586  psgnunilem2  19613  odf1o2  19691  sylow1lem1  19716  odcau  19722  pgpfi  19723  pgpssslw  19732  fislw  19743  efgtlen  19844  efginvrel2  19845  efgrelexlemb  19868  efgredeu  19870  efgcpbllemb  19873  frgpup1  19893  lt6abl  20013  gsum2d  20090  gsum2d2lem  20091  gsum2d2  20092  telgsumfzslem  20106  dmdprdsplit2lem  20165  ablfacrp  20186  pgpfac1lem3  20197  gsummgp0  20449  irredrmul  20559  subsubrng  20716  subsubrg  20751  rngcinv  20790  ringcinv  20824  fldhmsubc  20942  islss4  21137  lspextmo  21231  lspsnat  21323  prmirredlem  21676  znf1o  21755  znidomb  21765  frgpcyg  21777  psgnghm  21784  psgndiflemB  21804  frlmlbs  22001  frlmup1  22002  lindfind  22020  islindf3  22030  lindfmm  22031  issubassa3  22070  resspsradd  22178  resspsrmul  22179  psdmul  22383  coe1tmmul2  22491  pf1ind  22569  mamulid  22652  mat1dimelbas  22682  mdetdiaglem  22809  mdetralt2  22820  mndifsplit  22847  smadiadetglem2  22883  1elcpmat  22926  pmatcollpw3lem  22994  chfacfisf  23065  chfacfisfcpmat  23066  chfacffsupp  23067  chfacfscmulfsupp  23070  chfacfscmulgsum  23071  chfacfpmmulfsupp  23074  chfacfpmmulgsum  23075  chfacfpmmulgsum2  23076  cayhamlem1  23077  cpmadugsumlemF  23087  cayleyhamilton1  23103  tgcl  23180  pptbas  23219  clsval2  23261  mretopd  23303  lmbr2  23470  cncls2  23484  nrmsep  23568  regsep2  23587  cmpsublem  23610  cmpsub  23611  tgcmp  23612  uncmp  23614  hauscmplem  23617  iunconnlem  23638  1stcrest  23664  2ndcctbss  23667  2ndcsep  23671  dis2ndc  23672  hausllycmp  23706  dislly  23709  kgentopon  23750  1stckgen  23766  kgencn3  23770  ptpjpre1  23783  ptbasin  23789  ptpjopn  23824  dfac14  23830  ptcnplem  23833  txcn  23838  txindis  23846  txdis1cn  23847  ptrescn  23851  txcmplem1  23853  txcmp  23855  txhaus  23859  txlm  23860  tx1stc  23862  txkgen  23864  xkococn  23872  qtopcn  23926  kqreglem1  23953  kqreglem2  23954  kqnrmlem1  23955  kqnrmlem2  23956  hmeoimaf1o  23982  reghmph  24005  nrmhmph  24006  txhmeo  24015  ptuncnv  24019  filconn  24095  fbasrn  24096  fmfnfmlem2  24167  flimfnfcls  24240  cnpfcfi  24252  alexsublem  24256  alexsubALTlem2  24260  alexsubALTlem3  24261  alexsubALTlem4  24262  alexsubALT  24263  ptcmplem3  24266  cnextfval  24274  tsmsxp  24367  imasdsf1olem  24585  bl2in  24612  blssps  24636  blss  24637  blssexps  24638  blssex  24639  blcld  24717  stdbdxmet  24727  met1stc  24733  prdsxmslem2  24741  metcnp3  24752  metcnpi3  24758  txmetcnp  24759  nmo0  24947  nmoid  24954  icccmplem1  25035  icccmp  25038  xrge0tsms  25047  metdseq0  25067  cnheiborlem  25168  cnheibor  25169  cnllycmp  25170  pcoval2  25230  cmetcaulem  25502  iscmet3lem1  25505  iscmet3lem2  25506  equivcau  25514  lmcau  25527  cncmet  25536  ivthlem2  25666  ivthlem3  25667  ovoliunlem2  25717  ovolscalem2  25728  uniioombl  25803  dyaddisj  25810  opnmbllem  25815  volivth  25821  ismbfd  25853  ismbf3d  25868  mbfimaopnlem  25869  mbfinf  25879  itg1addlem4  25913  mbfi1fseqlem1  25929  mbfi1fseqlem3  25931  mbfi1fseqlem4  25932  mbfi1fseqlem5  25933  mbfi1fseqlem6  25934  itg2seq  25956  itg2lea  25958  itg2split  25963  itg2cnlem1  25975  bddiblnc  26056  limciun  26108  dvmptfsum  26189  rolle  26204  c1lip1  26211  dvcnvrelem1  26231  dvcnvre  26233  dvcvx  26234  itgsubst  26263  tdeglem4  26272  mdegmullem  26290  plyco0  26404  coemullem  26462  dgreq0  26477  dgrmul  26482  dgrco  26487  elqaalem2  26536  aannenlem1  26546  aaliou3lem9  26568  ulmres  26606  ulmshftlem  26607  angneg  27023  dcubic  27066  cxploglim  27197  cxploglim2  27198  scvxcvx  27205  lgamgulmlem5  27252  lgamcvg2  27274  ftalem2  27293  basellem3  27302  basellem4  27303  sqff1o  27401  fsumdvdsdiaglem  27402  dvdsflsumcom  27407  mpodvdsmulf1o  27413  dvdsmulf1o  27415  fsumvma2  27433  logfac2  27436  logfacrlim  27443  logexprlim  27444  dchrelbasd  27458  lgsne0  27554  lgsqrlem2  27566  lgsqrmodndvds  27572  gausslemma2dlem1a  27584  lgseisenlem2  27595  lgsquadlem1  27599  lgsquadlem2  27600  lgsquadlem3  27601  lgsquad2lem2  27604  2sqlem8  27645  2sqlem11  27648  2sqreultlem  27666  2sqreunnltlem  27669  chpo1ubb  27700  vmadivsum  27701  rplogsumlem2  27704  rpvmasumlem  27706  dchrmusum2  27713  dchrvmasumlem1  27714  dchrisum0fno1  27730  dchrisum0re  27732  dchrisum0lem1  27735  dchrisum0lem2  27737  dchrisum0lem3  27738  dchrisum0  27739  mulogsumlem  27750  mulog2sumlem2  27754  vmalogdivsum2  27757  logsqvma  27761  log2sumbnd  27763  selberglem3  27766  selberg  27767  selberg2lem  27769  selberg2b  27771  selberg3lem2  27777  pntrmax  27783  pntrsumo1  27784  pntlemn  27819  pntlemp  27829  qabvle  27844  ostthlem1  27846  ostthlem2  27847  ostth2lem2  27853  ostth3  27857  ltsres  27881  nosupno  27922  nosupbnd2  27935  noinfno  27937  noinfbnd2  27950  etaslts  28041  cuteq1  28065  addsproplem2  28218  mulsval  28357  precsexlem11  28465  n0fincut  28603  zmulscld  28645  bdayfinbndlem1  28715  idmot  28861  plngval  29114  brbtwn2  29314  colinearalglem4  29318  colinearalg  29319  ax5seglem9  29346  axpaschlem  29349  axcontlem2  29374  axcontlem7  29379  axcontlem8  29380  eengtrkg  29395  upgr1eopALT  29526  uspgredg2vlem  29635  subumgr  29700  nbgr0edglem  29768  edgnbusgreu  29779  nb3grprlem1  29792  wlkl1loop  30049  pthdivtx  30143  usgr2pth  30181  crctcshwlkn0  30241  wlklnwwlkln1  30288  wwlksnext  30313  clwwlkccatlem  30411  clwlkclwwlklem2a  30420  clwwlkinwwlk  30462  clwwlkn1loopb  30465  clwwlkf  30469  wwlksext2clwwlk  30479  wwlksubclwwlk  30480  clwwlknscsh  30484  clwwlknon1  30519  clwwlknonex2e  30532  1conngr  30620  n4cyclfrgr  30717  numclwwlk2lem1lem  30768  2clwwlk2clwwlk  30776  numclwwlk1lem2f1  30783  numclwlk1lem1  30795  numclwwlk2lem1  30802  numclwlk2lem2f  30803  numclwwlk7  30817  frgrogt3nreg  30823  grpoidinvlem1  30931  grpoidinvlem3  30933  grporcan  30945  nmlnoubi  31223  blocnilem  31231  ipblnfi  31282  htthlem  31344  ocsh  31710  shmodsi  31816  pjhthlem2  31819  5oalem2  32082  eigposi  32263  nmopub2tALT  32336  nmfnleub2  32353  nmcexi  32453  nmopcoi  32522  kbass3  32545  mdslmd1lem1  32752  mdslmd1lem2  32753  chirredlem2  32818  chirredlem4  32820  mdsymlem3  32832  mdsymlem5  32834  sumdmdii  32842  sumdmdlem  32845  sumdmdlem2  32846  foresf1o  32925  disjxpin  33008  1stpreimas  33126  resf1o  33149  nn0xmulclb  33190  wrdt2ind  33343  xrge0tsmsd  33461  gsumvsca1  33614  gsumvsca2  33615  islinds5  33750  1arithidomlem2  33894  mplvrpmmhm  34004  irngnzply1  34149  mdetpmtr1  34281  mdetpmtr2  34282  pstmxmet  34355  qqhghm  34446  qqhrhm  34447  esumpcvgval  34536  volmeas  34690  imambfm  34721  dya2iocnrect  34740  oddpwdc  34813  sseqf  34851  orvcgteel  34927  orvclteel  34932  ballotlemsf1o  34973  bnj1110  35439  bnj1118  35441  txpconn  35765  connpconn  35768  cnllysconn  35778  rellysconn  35784  cvmsss2  35807  cvmlift2lem9  35844  satf00  35907  fmlasuc  35919  mrsubfval  36041  mppsval  36105  dfon2lem6  36319  wzel  36355  ifscgr  36577  cgrxfr  36588  btwnconn1lem5  36624  btwnconn1lem6  36625  btwnconn1lem12  36631  brsegle  36641  finminlem  36890  nn0prpwlem  36894  fnessref  36929  refssfne  36930  neibastop1  36931  topjoin  36937  fnemeet2  36939  weiunse  37040  mh-inf3f1  37113  bj-prmoore  37818  bj-finsumval0  37990  topdifinffinlem  38054  lindsadd  38325  matunitlindflem2  38329  poimirlem28  38360  poimirlem32  38364  opnmbllem0  38368  mblfinlem1  38369  mblfinlem4  38372  ismblfin  38373  mbfresfi  38378  itg2addnclem  38383  itg2addnclem3  38385  itg2addnc  38386  unirep  38427  frinfm  38448  sdclem2  38455  geomcau  38472  istotbnd3  38484  sstotbnd2  38487  sstotbnd  38488  sstotbnd3  38489  totbndbnd  38502  cntotbnd  38509  ismtyres  38521  heibor1lem  38522  heiborlem1  38524  heiborlem8  38531  ismndo1  38586  isdivrngo  38663  unichnidl  38744  erimeq2  39474  cvlcvr1  40175  ishlat3N  40190  llnmlplnN  40375  islvol2aN  40428  4atlem4c  40437  4atlem4d  40438  isline2  40610  isline3  40612  linepsubclN  40787  lhpexle3lem  40847  lhpjat2  40857  cdlemd4  41037  cdleme0cq  41051  cdleme32fva  41273  cdleme32fvaw  41275  tendo0mul  41662  tendo0mulr  41663  diameetN  41892  dvhvaddcl  41931  dvhvaddcomN  41932  cdlemm10N  41954  dvadiaN  41964  djavalN  41971  dihvalcqat  42075  dihopelvalcpre  42084  djhval  42234  dihjat1lem  42264  sticksstones11  42985  sticksstones22  42997  remul01  43245  zaddcom  43315  zmulcom  43319  fidomncyc  43380  evlselvlem  43397  evlselv  43398  fsuppind  43399  mhpind  43403  prjspertr  43414  prjsprellsp  43420  elrfi  43502  nacsfix  43520  fzsplit1nn0  43562  eldioph2  43570  lzenom  43578  irrapxlem3  43628  pellexlem5  43637  pell1234qrne0  43657  pell1234qrmulcl  43659  pell14qrdich  43673  pell1qrge1  43674  pellqrex  43683  reglogltb  43695  reglogleb  43696  rmxypairf1o  43715  rmxycomplete  43721  monotoddzzfi  43746  congadd  43770  congsym  43772  acongrep  43784  jm2.19lem3  43795  jm2.19lem4  43796  jm2.22  43799  jm2.25  43803  expdiophlem1  43825  wepwsolem  43846  kelac1  43867  lmhmfgsplit  43890  pwslnm  43898  hbtlem6  43933  hbt  43934  mon1psubm  44003  deg1mhm  44004  omord2lim  44104  succlg  44132  onmcl  44135  ofoafo  44160  ofoacom  44165  fzunt  44258  fzuntd  44259  fzunt1d  44260  fzuntgd  44261  iunrelexp0  44505  dssmapnvod  44823  gsumws3  44999  gsumws4  45000  mulltgt0  45819  fnchoice  45826  disjrnmpt2  45983  fzisoeu  46096  fsumiunss  46368  climinf  46399  mullimc  46409  mullimcf  46416  stoweidlem14  46805  stoweidlem17  46808  stoweidlem34  46825  stoweidlem50  46841  fourierdlem42  46940  fourierdlem62  46959  fourierdlem71  46968  fourierdlem76  46973  qndenserrnbllem  47085  subsaliuncl  47149  sge0resplit  47197  3f1oss1  47889  2reu8i  47927  addmodne  48164  fundcmpsurinjpreimafv  48234  iccpartigtl  48249  prproropf1olem2  48330  prproropf1olem4  48332  paireqne  48337  prmdvdsfmtnof1lem2  48414  nprmdvdsfacm1  48453  bgoldbtbndlem3  48649  bgoldbtbnd  48651  grimcnv  48730  gricushgr  48759  cycldlenngric  48770  grimedg  48777  grtrimap  48790  isubgr3stgrlem6  48813  isubgr3stgrlem7  48814  isubgr3stgrlem8  48815  isubgr3stgrlem9  48816  grlimfn  48821  gpgedg2iv  48909  gpg5nbgrvtx03starlem2  48911  gpg5nbgrvtx13starlem2  48914  uspgrsprf1  48989  isassintop  49051  2zlidl  49081  2zrngnmrid  49097  rngcinvALTV  49117  funcringcsetcALTV2lem9  49139  ringcinvALTV  49151  funcringcsetclem9ALTV  49162  fldhmsubcALTV  49174  gsumlsscl  49236  lincsum  49285  lindslinindsimp1  49313  lindslinindimp2lem4  49317  lincresunitlem2  49332  elfzolborelfzop1  49375  elbigo2  49408  digexp  49463  dig1  49464  nn0sumshdiglemB  49476  1arymaptf1  49498  2arymaptf1  49509  itcoval1  49519  itcoval2  49520  itcoval3  49521  itcovalsucov  49524  ackvalsuc1mpt  49534  itschlc0xyqsol  49623  brab2dd  49682  dmrnxp  49691  xpco2  49711  initopropd  50097  termopropd  50098  zeroopropd  50099  prcofpropd  50233  thincciso  50307  indthinc  50316  indthincALT  50317  oduoppcciso  50420  lanpropd  50469  ranpropd  50470