Theorem ad2antrl 724

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

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  simprl  767  simprll  775  simprlr  776  simprl1  1216  simprl2  1217  simprl3  1218  disjxiun  5144  reusv2lem4  5398  axprlem5  5424  fr2nr  5653  somin1  6133  tz7.7  6389  f1oprg  6877  soisores  7326  elovmporab1w  7655  elovmporab1  7656  sorpssi  7721  onint  7780  ordsucelsuc  7812  elxp5  7916  wemoiso  7962  wemoiso2  7963  el2xptp0  8024  frxp2  8132  frxp3  8139  ressuppss  8170  fprlem1  8287  tz7.48lem  8443  oalimcl  8562  oeeui  8604  oaabs2  8650  omabs  8652  swoer  8735  ralxpmap  8892  pw2f1olem  9078  enfixsn  9083  mapxpen  9145  mapunen  9148  php  9212  unxpdomlem2  9253  unxpdomlem3  9254  findcard3OLD  9288  isfinite2  9303  domunfican  9322  fodomfi  9327  fissuni  9359  fipreima  9360  indexfi  9362  fsuppsssupp  9381  marypha1lem  9430  marypha2  9436  supmo  9449  infmo  9492  oieu  9536  brwdom2  9570  ixpiunwdom  9587  cantnfval2  9666  cantnfle  9668  cantnflt  9669  cantnf  9690  wemapwe  9694  cnfcom  9697  frrlem15  9754  rankonidlem  9825  r1pwcl  9844  eldju2ndl  9921  eldju2ndr  9922  djuun  9923  infxpenlem  10010  infxpenc2lem1  10016  fseqenlem1  10021  dfac8clem  10029  mappwen  10109  dfac3  10118  dfac5  10125  dfac12lem3  10142  infunsdom  10211  coftr  10270  ssfin4  10307  domfin4  10308  fin23lem26  10322  fin23lem22  10324  fin23lem28  10337  fin23lem32  10341  fin23lem40  10348  isf32lem5  10354  compssiso  10371  isf34lem4  10374  isfin1-3  10383  fin1a2lem13  10409  hsmexlem2  10424  hsmexlem4  10426  zorn2lem1  10493  ttukeylem6  10511  iundom2g  10537  konigthlem  10565  pwcfsdom  10580  fpwwe2lem11  10638  fpwwe2  10640  pwfseqlem3  10657  winalim2  10693  r1wunlim  10734  inttsk  10771  inar1  10772  grur1  10817  nqereq  10932  ltexprlem7  11039  prlem936  11044  00id  11393  addlid  11401  ltord1  11744  divdiv1  11929  divdiv2  11930  conjmul  11935  ltdivmul  12093  ledivmul  12094  lt2mul2div  12096  ltdiv23  12109  lediv23  12110  lediv12a  12111  ledivp1  12120  negfi  12167  nn0nndivcl  12547  nn0ge0div  12635  peano2uz2  12654  peano5uzi  12655  eluzp1m1  12852  qbtwnre  13182  xralrple  13188  xleadd1a  13236  xmulge0  13267  xmulass  13270  xlemul1a  13271  iooshf  13407  divelunit  13475  eluzgtdifelfzo  13698  modadd1  13877  modmul1  13893  seqcl2  13990  seqfveq2  13994  seqid2  14018  seqhomo  14019  seqdistr  14023  mulexpz  14072  leexp2r  14143  expnlbnd2  14201  expmulnbnd  14202  hashmap  14399  hashfun  14401  hashbclem  14415  hashfacen  14417  hashfacenOLD  14418  hashf1lem2  14421  hashf1  14422  ccatsymb  14536  swrdwrdsymb  14616  swrdsb0eq  14617  ccatpfx  14655  swrdswrd  14659  wrdind  14676  wrd2ind  14677  swrdccatin1  14679  swrdccatin2  14683  pfxccatin12lem2  14685  pfxccatin12  14687  swrdccat  14689  repswswrd  14738  0csh0  14747  cshwidxmod  14757  2cshw  14767  cshweqrep  14775  relexp0g  14973  relexpsucnnr  14976  relexpindlem  15014  01sqrexlem1  15193  01sqrexlem6  15198  rlim  15443  rlimclim1  15493  climsup  15620  caurcvg2  15628  caucvgb  15630  iseralt  15635  sumss  15674  fsum2dlem  15720  mptfzshft  15728  modfsummod  15744  o1fsum  15763  incexclem  15786  divrcnv  15802  flo1  15804  fprodrev  15925  fprod2dlem  15928  ruclem6  16182  moddvds  16212  dvdsaddre2b  16254  dvdsflip  16264  addmodlteqALT  16272  nn0o  16330  fldivndvdslt  16361  bitsf1ocnv  16389  bitsf1  16391  sadcaddlem  16402  bezoutlem2  16486  bezoutlem4  16488  lcmgcdlem  16547  prmind2  16626  isprm5  16648  isprm6  16655  prmdvdsncoprmbd  16667  cncongrprm  16669  hashdvds  16712  crth  16715  eulerthlem2  16719  prmdiveq  16723  hashgcdlem  16725  hashgcdeq  16726  iserodd  16772  pclem  16775  pcprendvds2  16778  pcexp  16796  pcneg  16811  pc2dvds  16816  pcmpt  16829  prmpwdvds  16841  pockthg  16843  prmreclem5  16857  4sqlem11  16892  ramub2  16951  ramubcl  16955  ram0  16959  ramub1lem2  16964  ramcl  16966  prmgaplem3  16990  prmgaplem6  16993  setscom  17117  sscpwex  17766  initoeu2  17970  setcinv  18044  funcestrcsetclem9  18104  funcsetcestrclem9  18119  fullsetcestrc  18122  1stfcl  18153  2ndfcl  18154  hofpropd  18224  isacs3lem  18499  isacs4lem  18501  acsmap2d  18512  subsubmgm  18635  submnd0  18688  subsubm  18733  insubm  18735  frmdup1  18781  frmdup3lem  18783  sgrp2nmndlem2  18841  isgrpinv  18914  subsubg  19065  cycsubgcl  19121  conjghm  19163  qusghm  19169  gsumwrev  19274  gsmsymgrfixlem1  19336  symgfixelsi  19344  symgsssg  19376  symgfisg  19377  psgnunilem2  19404  odf1o2  19482  sylow1lem1  19507  odcau  19513  pgpfi  19514  pgpssslw  19523  fislw  19534  efgtlen  19635  efginvrel2  19636  efgrelexlemb  19659  efgredeu  19661  efgcpbllemb  19664  frgpup1  19684  lt6abl  19804  gsum2d  19881  gsum2d2lem  19882  gsum2d2  19883  telgsumfzslem  19897  dmdprdsplit2lem  19956  ablfacrp  19977  pgpfac1lem3  19988  gsummgp0  20206  irredrmul  20318  subsubrng  20451  subsubrg  20488  islss4  20717  lspextmo  20811  lspsnat  20903  prmirredlem  21243  znf1o  21326  znidomb  21336  frgpcyg  21348  psgnghm  21352  psgndiflemB  21372  frlmlbs  21571  frlmup1  21572  lindfind  21590  islindf3  21600  lindfmm  21601  issubassa3  21639  resspsradd  21755  resspsrmul  21756  coe1tmmul2  22018  pf1ind  22094  mamulid  22163  mat1dimelbas  22193  mdetdiaglem  22320  mdetralt2  22331  mndifsplit  22358  smadiadetglem2  22394  1elcpmat  22437  pmatcollpw3lem  22505  chfacfisf  22576  chfacfisfcpmat  22577  chfacffsupp  22578  chfacfscmulfsupp  22581  chfacfscmulgsum  22582  chfacfpmmulfsupp  22585  chfacfpmmulgsum  22586  chfacfpmmulgsum2  22587  cayhamlem1  22588  cpmadugsumlemF  22598  cayleyhamilton1  22614  tgcl  22692  pptbas  22731  clsval2  22774  mretopd  22816  lmbr2  22983  cncls2  22997  nrmsep  23081  regsep2  23100  cmpsublem  23123  cmpsub  23124  tgcmp  23125  uncmp  23127  hauscmplem  23130  iunconnlem  23151  1stcrest  23177  2ndcctbss  23179  2ndcsep  23183  dis2ndc  23184  hausllycmp  23218  dislly  23221  kgentopon  23262  1stckgen  23278  kgencn3  23282  ptpjpre1  23295  ptbasin  23301  ptpjopn  23336  dfac14  23342  ptcnplem  23345  txcn  23350  txindis  23358  txdis1cn  23359  ptrescn  23363  txcmplem1  23365  txcmp  23367  txhaus  23371  txlm  23372  tx1stc  23374  txkgen  23376  xkococn  23384  qtopcn  23438  kqreglem1  23465  kqreglem2  23466  kqnrmlem1  23467  kqnrmlem2  23468  hmeoimaf1o  23494  reghmph  23517  nrmhmph  23518  txhmeo  23527  ptuncnv  23531  filconn  23607  fbasrn  23608  fmfnfmlem2  23679  flimfnfcls  23752  cnpfcfi  23764  alexsublem  23768  alexsubALTlem2  23772  alexsubALTlem3  23773  alexsubALTlem4  23774  alexsubALT  23775  ptcmplem3  23778  cnextfval  23786  tsmsxp  23879  imasdsf1olem  24099  bl2in  24126  blssps  24150  blss  24151  blssexps  24152  blssex  24153  blcld  24234  stdbdxmet  24244  met1stc  24250  prdsxmslem2  24258  metcnp3  24269  metcnpi3  24275  txmetcnp  24276  nmo0  24472  nmoid  24479  icccmplem1  24558  icccmp  24561  xrge0tsms  24570  metdseq0  24590  cnheiborlem  24700  cnheibor  24701  cnllycmp  24702  pcoval2  24763  cmetcaulem  25036  iscmet3lem1  25039  iscmet3lem2  25040  equivcau  25048  lmcau  25061  cncmet  25070  ivthlem2  25201  ivthlem3  25202  ovoliunlem2  25252  ovolscalem2  25263  uniioombl  25338  dyaddisj  25345  opnmbllem  25350  volivth  25356  ismbfd  25388  ismbf3d  25403  mbfimaopnlem  25404  mbfinf  25414  itg1addlem4  25448  itg1addlem4OLD  25449  mbfi1fseqlem1  25465  mbfi1fseqlem3  25467  mbfi1fseqlem4  25468  mbfi1fseqlem5  25469  mbfi1fseqlem6  25470  itg2seq  25492  itg2lea  25494  itg2split  25499  itg2cnlem1  25511  bddiblnc  25591  limciun  25643  dvmptfsum  25727  rolle  25742  c1lip1  25749  dvcnvrelem1  25769  dvcnvre  25771  dvcvx  25772  itgsubst  25801  tdeglem4  25812  tdeglem4OLD  25813  mdegmullem  25831  plyco0  25941  coemullem  25999  dgreq0  26015  dgrmul  26020  dgrco  26025  elqaalem2  26069  aannenlem1  26077  aaliou3lem9  26099  ulmres  26136  ulmshftlem  26137  angneg  26544  dcubic  26587  cxploglim  26718  cxploglim2  26719  scvxcvx  26726  lgamgulmlem5  26773  lgamcvg2  26795  ftalem2  26814  basellem3  26823  basellem4  26824  sqff1o  26922  fsumdvdsdiaglem  26923  dvdsflsumcom  26928  dvdsmulf1o  26934  fsumvma2  26953  logfac2  26956  logfacrlim  26963  logexprlim  26964  dchrelbasd  26978  lgsne0  27074  lgsqrlem2  27086  lgsqrmodndvds  27092  gausslemma2dlem1a  27104  lgseisenlem2  27115  lgsquadlem1  27119  lgsquadlem2  27120  lgsquadlem3  27121  lgsquad2lem2  27124  2sqlem8  27165  2sqlem11  27168  2sqreultlem  27186  2sqreunnltlem  27189  chpo1ubb  27220  vmadivsum  27221  rplogsumlem2  27224  rpvmasumlem  27226  dchrmusum2  27233  dchrvmasumlem1  27234  dchrisum0fno1  27250  dchrisum0re  27252  dchrisum0lem1  27255  dchrisum0lem2  27257  dchrisum0lem3  27258  dchrisum0  27259  mulogsumlem  27270  mulog2sumlem2  27274  vmalogdivsum2  27277  logsqvma  27281  log2sumbnd  27283  selberglem3  27286  selberg  27287  selberg2lem  27289  selberg2b  27291  selberg3lem2  27297  pntrmax  27303  pntrsumo1  27304  pntlemn  27339  pntlemp  27349  qabvle  27364  ostthlem1  27366  ostthlem2  27367  ostth2lem2  27373  ostth3  27377  sltres  27401  nosupno  27442  nosupbnd2  27455  noinfno  27457  noinfbnd2  27470  etasslt  27551  cuteq1  27571  addsproplem2  27692  mulsval  27804  precsexlem11  27902  idmot  28055  brbtwn2  28430  colinearalglem4  28434  colinearalg  28435  ax5seglem9  28462  axpaschlem  28465  axcontlem2  28490  axcontlem7  28495  axcontlem8  28496  eengtrkg  28511  upgr1eopALT  28644  uspgredg2vlem  28747  subumgr  28812  nbgr0vtxlem  28879  edgnbusgreu  28891  nb3grprlem1  28904  wlkl1loop  29162  pthdivtx  29253  usgr2pth  29288  crctcshwlkn0  29342  wlklnwwlkln1  29389  wwlksnext  29414  clwwlkccatlem  29509  clwlkclwwlklem2a  29518  clwwlkinwwlk  29560  clwwlkn1loopb  29563  clwwlkf  29567  wwlksext2clwwlk  29577  wwlksubclwwlk  29578  clwwlknscsh  29582  clwwlknon1  29617  clwwlknonex2e  29630  1conngr  29714  n4cyclfrgr  29811  numclwwlk2lem1lem  29862  2clwwlk2clwwlk  29870  numclwwlk1lem2f1  29877  numclwlk1lem1  29889  numclwwlk2lem1  29896  numclwlk2lem2f  29897  numclwwlk7  29911  frgrogt3nreg  29917  grpoidinvlem1  30024  grpoidinvlem3  30026  grporcan  30038  nmlnoubi  30316  blocnilem  30324  ipblnfi  30375  htthlem  30437  ocsh  30803  shmodsi  30909  pjhthlem2  30912  5oalem2  31175  eigposi  31356  nmopub2tALT  31429  nmfnleub2  31446  nmcexi  31546  nmopcoi  31615  kbass3  31638  mdslmd1lem1  31845  mdslmd1lem2  31846  chirredlem2  31911  chirredlem4  31913  mdsymlem3  31925  mdsymlem5  31927  sumdmdii  31935  sumdmdlem  31938  sumdmdlem2  31939  foresf1o  32009  disjxpin  32086  1stpreimas  32194  resf1o  32222  nn0xmulclb  32251  wrdt2ind  32384  xrge0tsmsd  32479  gsumvsca1  32641  gsumvsca2  32642  islinds5  32754  irngnzply1  33044  mdetpmtr1  33101  mdetpmtr2  33102  pstmxmet  33175  qqhghm  33266  qqhrhm  33267  esumpcvgval  33374  volmeas  33527  imambfm  33559  dya2iocnrect  33578  oddpwdc  33651  sseqf  33689  orvcgteel  33764  orvclteel  33769  ballotlemsf1o  33810  bnj1110  34291  bnj1118  34293  f1resveqaeq  34386  txpconn  34521  connpconn  34524  cnllysconn  34534  rellysconn  34540  cvmsss2  34563  cvmlift2lem9  34600  satf00  34663  fmlasuc  34675  mrsubfval  34797  mppsval  34861  dfon2lem6  35064  wzel  35100  ifscgr  35320  cgrxfr  35331  btwnconn1lem5  35367  btwnconn1lem6  35368  btwnconn1lem12  35374  brsegle  35384  finminlem  35506  nn0prpwlem  35510  fnessref  35545  refssfne  35546  neibastop1  35547  topjoin  35553  fnemeet2  35555  bj-prmoore  36299  bj-finsumval0  36469  topdifinffinlem  36531  lindsadd  36784  matunitlindflem2  36788  poimirlem28  36819  poimirlem32  36823  opnmbllem0  36827  mblfinlem1  36828  mblfinlem4  36831  ismblfin  36832  mbfresfi  36837  itg2addnclem  36842  itg2addnclem3  36844  itg2addnc  36845  unirep  36885  frinfm  36906  sdclem2  36913  geomcau  36930  istotbnd3  36942  sstotbnd2  36945  sstotbnd  36946  sstotbnd3  36947  totbndbnd  36960  cntotbnd  36967  ismtyres  36979  heibor1lem  36980  heiborlem1  36982  heiborlem8  36989  ismndo1  37044  isdivrngo  37121  unichnidl  37202  erimeq2  37851  cvlcvr1  38512  ishlat3N  38527  llnmlplnN  38713  islvol2aN  38766  4atlem4c  38775  4atlem4d  38776  isline2  38948  isline3  38950  linepsubclN  39125  lhpexle3lem  39185  lhpjat2  39195  cdlemd4  39375  cdleme0cq  39389  cdleme32fva  39611  cdleme32fvaw  39613  tendo0mul  40000  tendo0mulr  40001  diameetN  40230  dvhvaddcl  40269  dvhvaddcomN  40270  cdlemm10N  40292  dvadiaN  40302  djavalN  40309  dihvalcqat  40413  dihopelvalcpre  40422  djhval  40572  dihjat1lem  40602  sticksstones11  41278  sticksstones22  41290  metakunt15  41305  metakunt16  41306  f1o2d2  41361  evlselvlem  41460  evlselv  41461  fsuppind  41464  mhpind  41468  remul01  41582  zaddcom  41627  zmulcom  41631  prjspertr  41649  prjsprellsp  41655  elrfi  41734  nacsfix  41752  fzsplit1nn0  41794  eldioph2  41802  lzenom  41810  irrapxlem3  41864  pellexlem5  41873  pell1234qrne0  41893  pell1234qrmulcl  41895  pell14qrdich  41909  pell1qrge1  41910  pellqrex  41919  reglogltb  41931  reglogleb  41932  rmxypairf1o  41952  rmxycomplete  41958  monotoddzzfi  41983  congadd  42007  congsym  42009  acongrep  42021  jm2.19lem3  42032  jm2.19lem4  42033  jm2.22  42036  jm2.25  42040  expdiophlem1  42062  wepwsolem  42086  kelac1  42107  lmhmfgsplit  42130  pwslnm  42138  hbtlem6  42173  hbt  42174  mon1psubm  42250  deg1mhm  42251  omord2lim  42352  succlg  42380  onmcl  42383  ofoafo  42408  ofoacom  42413  fzunt  42508  fzuntd  42509  fzunt1d  42510  fzuntgd  42511  iunrelexp0  42755  dssmapnvod  43073  gsumws3  43250  gsumws4  43251  mulltgt0  44008  fnchoice  44015  disjrnmpt2  44185  fzisoeu  44308  fsumiunss  44589  climinf  44620  mullimc  44630  mullimcf  44637  stoweidlem14  45028  stoweidlem17  45031  stoweidlem34  45048  stoweidlem50  45064  fourierdlem42  45163  fourierdlem62  45182  fourierdlem71  45191  fourierdlem76  45196  qndenserrnbllem  45308  subsaliuncl  45372  sge0resplit  45420  upwrdfi  45899  2reu8i  46119  fundcmpsurinjpreimafv  46374  iccpartigtl  46389  prproropf1olem2  46470  prproropf1olem4  46472  paireqne  46477  prmdvdsfmtnof1lem2  46551  bgoldbtbndlem3  46773  bgoldbtbnd  46775  isomushgr  46792  isomuspgrlem2c  46796  uspgrsprf1  46823  isassintop  46886  2zlidl  46920  2zrngnmrid  46936  rngcinv  46967  rngcinvALTV  46979  ringcinv  47018  funcringcsetcALTV2lem9  47030  ringcinvALTV  47042  funcringcsetclem9ALTV  47053  fldhmsubc  47070  fldhmsubcALTV  47088  mndpsuppss  47135  gsumlsscl  47147  lincsum  47197  lindslinindsimp1  47225  lindslinindimp2lem4  47229  lincresunitlem2  47244  elfzolborelfzop1  47287  elbigo2  47325  digexp  47380  dig1  47381  nn0sumshdiglemB  47393  1arymaptf1  47415  2arymaptf1  47426  itcoval1  47436  itcoval2  47437  itcoval3  47438  itcovalsucov  47441  ackvalsuc1mpt  47451  itschlc0xyqsol  47540  thincciso  47756  indthinc  47759  indthincALT  47760