Theorem ad2antrl 727

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 716	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  770  simprll  778  simprlr  779  simprl1  1218  simprl2  1219  simprl3  1220  disjxiun  5163  reusv2lem4  5419  axprlem5  5445  fr2nr  5677  somin1  6165  tz7.7  6421  f1oprg  6907  soisores  7363  elovmporab1w  7697  elovmporab1  7698  sorpssi  7764  onint  7826  ordsucelsuc  7858  elxp5  7963  f1oabexg  7980  wemoiso  8014  wemoiso2  8015  el2xptp0  8077  frxp2  8185  frxp3  8192  ressuppss  8224  fprlem1  8341  tz7.48lem  8497  oalimcl  8616  oeeui  8658  nnaordex2  8695  oaabs2  8705  omabs  8707  swoer  8794  ralxpmap  8954  pw2f1olem  9142  enfixsn  9147  mapxpen  9209  mapunen  9212  php  9273  unxpdomlem2  9314  unxpdomlem3  9315  findcard3OLD  9347  isfinite2  9362  fodomfi  9378  domunfican  9389  fodomfiOLD  9398  fissuni  9427  fipreima  9428  indexfi  9430  fsuppsssupp  9450  marypha1lem  9502  marypha2  9508  supmo  9521  infmo  9564  oieu  9608  brwdom2  9642  ixpiunwdom  9659  cantnfval2  9738  cantnfle  9740  cantnflt  9741  cantnf  9762  wemapwe  9766  cnfcom  9769  frrlem15  9826  rankonidlem  9897  r1pwcl  9916  eldju2ndl  9993  eldju2ndr  9994  djuun  9995  infxpenlem  10082  infxpenc2lem1  10088  fseqenlem1  10093  dfac8clem  10101  mappwen  10181  dfac3  10190  dfac5  10198  dfac12lem3  10215  infunsdom  10282  coftr  10342  ssfin4  10379  domfin4  10380  fin23lem26  10394  fin23lem22  10396  fin23lem28  10409  fin23lem32  10413  fin23lem40  10420  isf32lem5  10426  compssiso  10443  isf34lem4  10446  isfin1-3  10455  fin1a2lem13  10481  hsmexlem2  10496  hsmexlem4  10498  zorn2lem1  10565  ttukeylem6  10583  iundom2g  10609  konigthlem  10637  pwcfsdom  10652  fpwwe2lem11  10710  fpwwe2  10712  pwfseqlem3  10729  winalim2  10765  r1wunlim  10806  inttsk  10843  inar1  10844  grur1  10889  nqereq  11004  ltexprlem7  11111  prlem936  11116  00id  11465  addlid  11473  ltord1  11816  divdiv1  12005  divdiv2  12006  conjmul  12011  ltdivmul  12170  ledivmul  12171  lt2mul2div  12173  ltdiv23  12186  lediv23  12187  lediv12a  12188  ledivp1  12197  negfi  12244  nn0nndivcl  12624  nn0ge0div  12712  peano2uz2  12731  peano5uzi  12732  eluzp1m1  12929  qbtwnre  13261  xralrple  13267  xleadd1a  13315  xmulge0  13346  xmulass  13349  xlemul1a  13350  iooshf  13486  divelunit  13554  eluzgtdifelfzo  13778  modadd1  13959  modmul1  13975  seqcl2  14071  seqfveq2  14075  seqid2  14099  seqhomo  14100  seqdistr  14104  mulexpz  14153  leexp2r  14224  expnlbnd2  14283  expmulnbnd  14284  hashmap  14484  hashfun  14486  hashbclem  14501  hashfacen  14503  hashf1lem2  14505  hashf1  14506  ccatsymb  14630  swrdwrdsymb  14710  swrdsb0eq  14711  ccatpfx  14749  swrdswrd  14753  wrdind  14770  wrd2ind  14771  swrdccatin1  14773  swrdccatin2  14777  pfxccatin12lem2  14779  pfxccatin12  14781  swrdccat  14783  repswswrd  14832  0csh0  14841  cshwidxmod  14851  2cshw  14861  cshweqrep  14869  relexp0g  15071  relexpsucnnr  15074  relexpindlem  15112  01sqrexlem1  15291  01sqrexlem6  15296  rlim  15541  rlimclim1  15591  climsup  15718  caurcvg2  15726  caucvgb  15728  iseralt  15733  sumss  15772  fsum2dlem  15818  mptfzshft  15826  modfsummod  15842  o1fsum  15861  incexclem  15884  divrcnv  15900  flo1  15902  fprodrev  16025  fprod2dlem  16028  ruclem6  16283  moddvds  16313  dvdsaddre2b  16355  dvdsflip  16365  addmodlteqALT  16373  nn0o  16431  fldivndvdslt  16462  bitsf1ocnv  16490  bitsf1  16492  sadcaddlem  16503  bezoutlem2  16587  bezoutlem4  16589  lcmgcdlem  16653  prmind2  16732  isprm5  16754  isprm6  16761  prmdvdsncoprmbd  16774  cncongrprm  16776  hashdvds  16822  crth  16825  eulerthlem2  16829  prmdiveq  16833  hashgcdlem  16835  hashgcdeq  16836  iserodd  16882  pclem  16885  pcprendvds2  16888  pcexp  16906  pcneg  16921  pc2dvds  16926  pcmpt  16939  prmpwdvds  16951  pockthg  16953  prmreclem5  16967  4sqlem11  17002  ramub2  17061  ramubcl  17065  ram0  17069  ramub1lem2  17074  ramcl  17076  prmgaplem3  17100  prmgaplem6  17103  setscom  17227  sscpwex  17876  initoeu2  18083  setcinv  18157  funcestrcsetclem9  18217  funcsetcestrclem9  18232  fullsetcestrc  18235  1stfcl  18266  2ndfcl  18267  hofpropd  18337  isacs3lem  18612  isacs4lem  18614  acsmap2d  18625  subsubmgm  18748  submnd0  18801  subsubm  18851  insubm  18853  frmdup1  18899  frmdup3lem  18901  sgrp2nmndlem2  18959  isgrpinv  19033  subsubg  19189  cycsubgcl  19246  conjghm  19289  qusghm  19295  gsumwrev  19409  gsmsymgrfixlem1  19469  symgfixelsi  19477  symgsssg  19509  symgfisg  19510  psgnunilem2  19537  odf1o2  19615  sylow1lem1  19640  odcau  19646  pgpfi  19647  pgpssslw  19656  fislw  19667  efgtlen  19768  efginvrel2  19769  efgrelexlemb  19792  efgredeu  19794  efgcpbllemb  19797  frgpup1  19817  lt6abl  19937  gsum2d  20014  gsum2d2lem  20015  gsum2d2  20016  telgsumfzslem  20030  dmdprdsplit2lem  20089  ablfacrp  20110  pgpfac1lem3  20121  gsummgp0  20341  irredrmul  20453  subsubrng  20589  subsubrg  20626  rngcinv  20659  ringcinv  20693  fldhmsubc  20808  islss4  20983  lspextmo  21078  lspsnat  21170  prmirredlem  21506  znf1o  21593  znidomb  21603  frgpcyg  21615  psgnghm  21621  psgndiflemB  21641  frlmlbs  21840  frlmup1  21841  lindfind  21859  islindf3  21869  lindfmm  21870  issubassa3  21909  resspsradd  22018  resspsrmul  22019  psdmul  22193  coe1tmmul2  22300  pf1ind  22380  mamulid  22468  mat1dimelbas  22498  mdetdiaglem  22625  mdetralt2  22636  mndifsplit  22663  smadiadetglem2  22699  1elcpmat  22742  pmatcollpw3lem  22810  chfacfisf  22881  chfacfisfcpmat  22882  chfacffsupp  22883  chfacfscmulfsupp  22886  chfacfscmulgsum  22887  chfacfpmmulfsupp  22890  chfacfpmmulgsum  22891  chfacfpmmulgsum2  22892  cayhamlem1  22893  cpmadugsumlemF  22903  cayleyhamilton1  22919  tgcl  22997  pptbas  23036  clsval2  23079  mretopd  23121  lmbr2  23288  cncls2  23302  nrmsep  23386  regsep2  23405  cmpsublem  23428  cmpsub  23429  tgcmp  23430  uncmp  23432  hauscmplem  23435  iunconnlem  23456  1stcrest  23482  2ndcctbss  23484  2ndcsep  23488  dis2ndc  23489  hausllycmp  23523  dislly  23526  kgentopon  23567  1stckgen  23583  kgencn3  23587  ptpjpre1  23600  ptbasin  23606  ptpjopn  23641  dfac14  23647  ptcnplem  23650  txcn  23655  txindis  23663  txdis1cn  23664  ptrescn  23668  txcmplem1  23670  txcmp  23672  txhaus  23676  txlm  23677  tx1stc  23679  txkgen  23681  xkococn  23689  qtopcn  23743  kqreglem1  23770  kqreglem2  23771  kqnrmlem1  23772  kqnrmlem2  23773  hmeoimaf1o  23799  reghmph  23822  nrmhmph  23823  txhmeo  23832  ptuncnv  23836  filconn  23912  fbasrn  23913  fmfnfmlem2  23984  flimfnfcls  24057  cnpfcfi  24069  alexsublem  24073  alexsubALTlem2  24077  alexsubALTlem3  24078  alexsubALTlem4  24079  alexsubALT  24080  ptcmplem3  24083  cnextfval  24091  tsmsxp  24184  imasdsf1olem  24404  bl2in  24431  blssps  24455  blss  24456  blssexps  24457  blssex  24458  blcld  24539  stdbdxmet  24549  met1stc  24555  prdsxmslem2  24563  metcnp3  24574  metcnpi3  24580  txmetcnp  24581  nmo0  24777  nmoid  24784  icccmplem1  24863  icccmp  24866  xrge0tsms  24875  metdseq0  24895  cnheiborlem  25005  cnheibor  25006  cnllycmp  25007  pcoval2  25068  cmetcaulem  25341  iscmet3lem1  25344  iscmet3lem2  25345  equivcau  25353  lmcau  25366  cncmet  25375  ivthlem2  25506  ivthlem3  25507  ovoliunlem2  25557  ovolscalem2  25568  uniioombl  25643  dyaddisj  25650  opnmbllem  25655  volivth  25661  ismbfd  25693  ismbf3d  25708  mbfimaopnlem  25709  mbfinf  25719  itg1addlem4  25753  itg1addlem4OLD  25754  mbfi1fseqlem1  25770  mbfi1fseqlem3  25772  mbfi1fseqlem4  25773  mbfi1fseqlem5  25774  mbfi1fseqlem6  25775  itg2seq  25797  itg2lea  25799  itg2split  25804  itg2cnlem1  25816  bddiblnc  25897  limciun  25949  dvmptfsum  26033  rolle  26048  c1lip1  26056  dvcnvrelem1  26076  dvcnvre  26078  dvcvx  26079  itgsubst  26110  tdeglem4  26119  mdegmullem  26137  plyco0  26251  coemullem  26309  dgreq0  26325  dgrmul  26330  dgrco  26335  elqaalem2  26380  aannenlem1  26388  aaliou3lem9  26410  ulmres  26449  ulmshftlem  26450  angneg  26864  dcubic  26907  cxploglim  27039  cxploglim2  27040  scvxcvx  27047  lgamgulmlem5  27094  lgamcvg2  27116  ftalem2  27135  basellem3  27144  basellem4  27145  sqff1o  27243  fsumdvdsdiaglem  27244  dvdsflsumcom  27249  mpodvdsmulf1o  27255  dvdsmulf1o  27257  fsumvma2  27276  logfac2  27279  logfacrlim  27286  logexprlim  27287  dchrelbasd  27301  lgsne0  27397  lgsqrlem2  27409  lgsqrmodndvds  27415  gausslemma2dlem1a  27427  lgseisenlem2  27438  lgsquadlem1  27442  lgsquadlem2  27443  lgsquadlem3  27444  lgsquad2lem2  27447  2sqlem8  27488  2sqlem11  27491  2sqreultlem  27509  2sqreunnltlem  27512  chpo1ubb  27543  vmadivsum  27544  rplogsumlem2  27547  rpvmasumlem  27549  dchrmusum2  27556  dchrvmasumlem1  27557  dchrisum0fno1  27573  dchrisum0re  27575  dchrisum0lem1  27578  dchrisum0lem2  27580  dchrisum0lem3  27581  dchrisum0  27582  mulogsumlem  27593  mulog2sumlem2  27597  vmalogdivsum2  27600  logsqvma  27604  log2sumbnd  27606  selberglem3  27609  selberg  27610  selberg2lem  27612  selberg2b  27614  selberg3lem2  27620  pntrmax  27626  pntrsumo1  27627  pntlemn  27662  pntlemp  27672  qabvle  27687  ostthlem1  27689  ostthlem2  27690  ostth2lem2  27696  ostth3  27700  sltres  27725  nosupno  27766  nosupbnd2  27779  noinfno  27781  noinfbnd2  27794  etasslt  27876  cuteq1  27896  addsproplem2  28021  mulsval  28153  precsexlem11  28259  zmulscld  28401  idmot  28563  brbtwn2  28938  colinearalglem4  28942  colinearalg  28943  ax5seglem9  28970  axpaschlem  28973  axcontlem2  28998  axcontlem7  29003  axcontlem8  29004  eengtrkg  29019  upgr1eopALT  29152  uspgredg2vlem  29258  subumgr  29323  nbgr0edglem  29391  edgnbusgreu  29402  nb3grprlem1  29415  wlkl1loop  29674  pthdivtx  29765  usgr2pth  29800  crctcshwlkn0  29854  wlklnwwlkln1  29901  wwlksnext  29926  clwwlkccatlem  30021  clwlkclwwlklem2a  30030  clwwlkinwwlk  30072  clwwlkn1loopb  30075  clwwlkf  30079  wwlksext2clwwlk  30089  wwlksubclwwlk  30090  clwwlknscsh  30094  clwwlknon1  30129  clwwlknonex2e  30142  1conngr  30226  n4cyclfrgr  30323  numclwwlk2lem1lem  30374  2clwwlk2clwwlk  30382  numclwwlk1lem2f1  30389  numclwlk1lem1  30401  numclwwlk2lem1  30408  numclwlk2lem2f  30409  numclwwlk7  30423  frgrogt3nreg  30429  grpoidinvlem1  30536  grpoidinvlem3  30538  grporcan  30550  nmlnoubi  30828  blocnilem  30836  ipblnfi  30887  htthlem  30949  ocsh  31315  shmodsi  31421  pjhthlem2  31424  5oalem2  31687  eigposi  31868  nmopub2tALT  31941  nmfnleub2  31958  nmcexi  32058  nmopcoi  32127  kbass3  32150  mdslmd1lem1  32357  mdslmd1lem2  32358  chirredlem2  32423  chirredlem4  32425  mdsymlem3  32437  mdsymlem5  32439  sumdmdii  32447  sumdmdlem  32450  sumdmdlem2  32451  foresf1o  32532  disjxpin  32610  1stpreimas  32717  resf1o  32744  nn0xmulclb  32778  wrdt2ind  32920  xrge0tsmsd  33041  gsumvsca1  33205  gsumvsca2  33206  islinds5  33360  1arithidomlem2  33529  irngnzply1  33691  mdetpmtr1  33769  mdetpmtr2  33770  pstmxmet  33843  qqhghm  33934  qqhrhm  33935  esumpcvgval  34042  volmeas  34195  imambfm  34227  dya2iocnrect  34246  oddpwdc  34319  sseqf  34357  orvcgteel  34432  orvclteel  34437  ballotlemsf1o  34478  bnj1110  34958  bnj1118  34960  f1resveqaeq  35061  txpconn  35200  connpconn  35203  cnllysconn  35213  rellysconn  35219  cvmsss2  35242  cvmlift2lem9  35279  satf00  35342  fmlasuc  35354  mrsubfval  35476  mppsval  35540  dfon2lem6  35752  wzel  35788  ifscgr  36008  cgrxfr  36019  btwnconn1lem5  36055  btwnconn1lem6  36056  btwnconn1lem12  36062  brsegle  36072  finminlem  36284  nn0prpwlem  36288  fnessref  36323  refssfne  36324  neibastop1  36325  topjoin  36331  fnemeet2  36333  weiunse  36434  bj-prmoore  37081  bj-finsumval0  37251  topdifinffinlem  37313  lindsadd  37573  matunitlindflem2  37577  poimirlem28  37608  poimirlem32  37612  opnmbllem0  37616  mblfinlem1  37617  mblfinlem4  37620  ismblfin  37621  mbfresfi  37626  itg2addnclem  37631  itg2addnclem3  37633  itg2addnc  37634  unirep  37674  frinfm  37695  sdclem2  37702  geomcau  37719  istotbnd3  37731  sstotbnd2  37734  sstotbnd  37735  sstotbnd3  37736  totbndbnd  37749  cntotbnd  37756  ismtyres  37768  heibor1lem  37769  heiborlem1  37771  heiborlem8  37778  ismndo1  37833  isdivrngo  37910  unichnidl  37991  erimeq2  38634  cvlcvr1  39295  ishlat3N  39310  llnmlplnN  39496  islvol2aN  39549  4atlem4c  39558  4atlem4d  39559  isline2  39731  isline3  39733  linepsubclN  39908  lhpexle3lem  39968  lhpjat2  39978  cdlemd4  40158  cdleme0cq  40172  cdleme32fva  40394  cdleme32fvaw  40396  tendo0mul  40783  tendo0mulr  40784  diameetN  41013  dvhvaddcl  41052  dvhvaddcomN  41053  cdlemm10N  41075  dvadiaN  41085  djavalN  41092  dihvalcqat  41196  dihopelvalcpre  41205  djhval  41355  dihjat1lem  41385  sticksstones11  42113  sticksstones22  42125  metakunt15  42176  metakunt16  42177  f1o2d2  42228  remul01  42383  zaddcom  42428  zmulcom  42432  fidomncyc  42490  evlselvlem  42541  evlselv  42542  fsuppind  42545  mhpind  42549  prjspertr  42560  prjsprellsp  42566  elrfi  42650  nacsfix  42668  fzsplit1nn0  42710  eldioph2  42718  lzenom  42726  irrapxlem3  42780  pellexlem5  42789  pell1234qrne0  42809  pell1234qrmulcl  42811  pell14qrdich  42825  pell1qrge1  42826  pellqrex  42835  reglogltb  42847  reglogleb  42848  rmxypairf1o  42868  rmxycomplete  42874  monotoddzzfi  42899  congadd  42923  congsym  42925  acongrep  42937  jm2.19lem3  42948  jm2.19lem4  42949  jm2.22  42952  jm2.25  42956  expdiophlem1  42978  wepwsolem  42999  kelac1  43020  lmhmfgsplit  43043  pwslnm  43051  hbtlem6  43086  hbt  43087  mon1psubm  43160  deg1mhm  43161  omord2lim  43262  succlg  43290  onmcl  43293  ofoafo  43318  ofoacom  43323  fzunt  43417  fzuntd  43418  fzunt1d  43419  fzuntgd  43420  iunrelexp0  43664  dssmapnvod  43982  gsumws3  44158  gsumws4  44159  mulltgt0  44922  fnchoice  44929  disjrnmpt2  45095  fzisoeu  45215  fsumiunss  45496  climinf  45527  mullimc  45537  mullimcf  45544  stoweidlem14  45935  stoweidlem17  45938  stoweidlem34  45955  stoweidlem50  45971  fourierdlem42  46070  fourierdlem62  46089  fourierdlem71  46098  fourierdlem76  46103  qndenserrnbllem  46215  subsaliuncl  46279  sge0resplit  46327  upwrdfi  46806  3f1oss1  46990  2reu8i  47028  fundcmpsurinjpreimafv  47282  iccpartigtl  47297  prproropf1olem2  47378  prproropf1olem4  47380  paireqne  47385  prmdvdsfmtnof1lem2  47459  bgoldbtbndlem3  47681  bgoldbtbnd  47683  uspgrimprop  47757  grimcnv  47763  gricushgr  47770  grimedg  47787  grtrimap  47797  grlimfn  47803  uspgrsprf1  47870  isassintop  47933  2zlidl  47963  2zrngnmrid  47979  rngcinvALTV  47999  funcringcsetcALTV2lem9  48021  ringcinvALTV  48033  funcringcsetclem9ALTV  48044  fldhmsubcALTV  48056  mndpsuppss  48096  gsumlsscl  48108  lincsum  48158  lindslinindsimp1  48186  lindslinindimp2lem4  48190  lincresunitlem2  48205  elfzolborelfzop1  48248  elbigo2  48286  digexp  48341  dig1  48342  nn0sumshdiglemB  48354  1arymaptf1  48376  2arymaptf1  48387  itcoval1  48397  itcoval2  48398  itcoval3  48399  itcovalsucov  48402  ackvalsuc1mpt  48412  itschlc0xyqsol  48501  thincciso  48716  indthinc  48719  indthincALT  48720