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  770  simprll  778  simprlr  779  simprl1  1219  simprl2  1220  simprl3  1221  disjxiun  5086  reusv2lem4  5337  axprlem5OLD  5366  fr2nr  5591  somin1  6079  tz7.7  6332  f1oprg  6808  soisores  7261  elovmporab1w  7593  elovmporab1  7594  sorpssi  7662  onint  7723  ordsucelsuc  7752  elxp5  7853  resf1extb  7864  f1oabexg  7872  wemoiso  7905  wemoiso2  7906  el2xptp0  7968  frxp2  8074  frxp3  8081  ressuppss  8113  fprlem1  8230  tz7.48lem  8360  oalimcl  8475  oeeui  8517  nnaordex2  8554  oaabs2  8564  omabs  8566  swoer  8653  ralxpmap  8820  pw2f1olem  8994  enfixsn  8999  mapxpen  9056  mapunen  9059  php  9116  unxpdomlem2  9141  unxpdomlem3  9142  isfinite2  9182  fodomfi  9196  domunfican  9206  fodomfiOLD  9214  fissuni  9241  fipreima  9242  indexfi  9244  fsuppsssupp  9265  marypha1lem  9317  marypha2  9323  supmo  9336  infmo  9381  oieu  9425  brwdom2  9459  ixpiunwdom  9476  cantnfval2  9559  cantnfle  9561  cantnflt  9562  cantnf  9583  wemapwe  9587  cnfcom  9590  frrlem15  9650  rankonidlem  9721  r1pwcl  9740  eldju2ndl  9817  eldju2ndr  9818  djuun  9819  infxpenlem  9904  infxpenc2lem1  9910  fseqenlem1  9915  dfac8clem  9923  mappwen  10003  dfac3  10012  dfac5  10020  dfac12lem3  10037  infunsdom  10104  coftr  10164  ssfin4  10201  domfin4  10202  fin23lem26  10216  fin23lem22  10218  fin23lem28  10231  fin23lem32  10235  fin23lem40  10242  isf32lem5  10248  compssiso  10265  isf34lem4  10268  isfin1-3  10277  fin1a2lem13  10303  hsmexlem2  10318  hsmexlem4  10320  zorn2lem1  10387  ttukeylem6  10405  iundom2g  10431  konigthlem  10459  pwcfsdom  10474  fpwwe2lem11  10532  fpwwe2  10534  pwfseqlem3  10551  winalim2  10587  r1wunlim  10628  inttsk  10665  inar1  10666  grur1  10711  nqereq  10826  ltexprlem7  10933  prlem936  10938  00id  11288  addlid  11296  ltord1  11643  divdiv1  11832  divdiv2  11833  conjmul  11838  ltdivmul  11997  ledivmul  11998  lt2mul2div  12000  ltdiv23  12013  lediv23  12014  lediv12a  12015  ledivp1  12024  negfi  12071  nn0nndivcl  12453  nn0ge0div  12542  peano2uz2  12561  peano5uzi  12562  eluzp1m1  12758  qbtwnre  13098  xralrple  13104  xleadd1a  13152  xmulge0  13183  xmulass  13186  xlemul1a  13187  iooshf  13326  divelunit  13394  eluzgtdifelfzo  13627  modadd1  13812  modmul1  13831  seqcl2  13927  seqfveq2  13931  seqid2  13955  seqhomo  13956  seqdistr  13960  mulexpz  14009  leexp2r  14081  expnlbnd2  14141  expmulnbnd  14142  hashmap  14342  hashfun  14344  hashbclem  14359  hashfacen  14361  hashf1lem2  14363  hashf1  14364  ccatsymb  14490  swrdwrdsymb  14570  swrdsb0eq  14571  ccatpfx  14608  swrdswrd  14612  wrdind  14629  wrd2ind  14630  swrdccatin1  14632  swrdccatin2  14636  pfxccatin12lem2  14638  pfxccatin12  14640  swrdccat  14642  repswswrd  14691  0csh0  14700  cshwidxmod  14710  2cshw  14720  cshweqrep  14728  relexp0g  14929  relexpsucnnr  14932  relexpindlem  14970  01sqrexlem1  15149  01sqrexlem6  15154  rlim  15402  rlimclim1  15452  climsup  15577  caurcvg2  15585  caucvgb  15587  iseralt  15592  sumss  15631  fsum2dlem  15677  mptfzshft  15685  modfsummod  15701  o1fsum  15720  incexclem  15743  divrcnv  15759  flo1  15761  fprodrev  15884  fprod2dlem  15887  ruclem6  16144  moddvds  16174  dvdsaddre2b  16218  dvdsflip  16228  addmodlteqALT  16236  nn0o  16294  fldivndvdslt  16327  bitsf1ocnv  16355  bitsf1  16357  sadcaddlem  16368  bezoutlem2  16451  bezoutlem4  16453  lcmgcdlem  16517  prmind2  16596  isprm5  16618  isprm6  16625  prmdvdsncoprmbd  16638  cncongrprm  16640  hashdvds  16686  crth  16689  eulerthlem2  16693  prmdiveq  16697  hashgcdlem  16699  hashgcdeq  16701  iserodd  16747  pclem  16750  pcprendvds2  16753  pcexp  16771  pcneg  16786  pc2dvds  16791  pcmpt  16804  prmpwdvds  16816  pockthg  16818  prmreclem5  16832  4sqlem11  16867  ramub2  16926  ramubcl  16930  ram0  16934  ramub1lem2  16939  ramcl  16941  prmgaplem3  16965  prmgaplem6  16968  setscom  17091  sscpwex  17722  initoeu2  17923  setcinv  17997  funcestrcsetclem9  18054  funcsetcestrclem9  18069  fullsetcestrc  18072  1stfcl  18103  2ndfcl  18104  hofpropd  18173  isacs3lem  18448  isacs4lem  18450  acsmap2d  18461  chnflenfi  18534  subsubmgm  18618  submnd0  18671  mndpsuppss  18673  subsubm  18724  insubm  18726  frmdup1  18772  frmdup3lem  18774  sgrp2nmndlem2  18832  isgrpinv  18906  subsubg  19062  cycsubgcl  19118  conjghm  19161  qusghm  19167  gsumwrev  19278  gsmsymgrfixlem1  19339  symgfixelsi  19347  symgsssg  19379  symgfisg  19380  psgnunilem2  19407  odf1o2  19485  sylow1lem1  19510  odcau  19516  pgpfi  19517  pgpssslw  19526  fislw  19537  efgtlen  19638  efginvrel2  19639  efgrelexlemb  19662  efgredeu  19664  efgcpbllemb  19667  frgpup1  19687  lt6abl  19807  gsum2d  19884  gsum2d2lem  19885  gsum2d2  19886  telgsumfzslem  19900  dmdprdsplit2lem  19959  ablfacrp  19980  pgpfac1lem3  19991  gsummgp0  20236  irredrmul  20345  subsubrng  20478  subsubrg  20513  rngcinv  20552  ringcinv  20586  fldhmsubc  20700  islss4  20895  lspextmo  20990  lspsnat  21082  prmirredlem  21409  znf1o  21488  znidomb  21498  frgpcyg  21510  psgnghm  21517  psgndiflemB  21537  frlmlbs  21734  frlmup1  21735  lindfind  21753  islindf3  21763  lindfmm  21764  issubassa3  21803  resspsradd  21912  resspsrmul  21913  psdmul  22081  coe1tmmul2  22190  pf1ind  22270  mamulid  22356  mat1dimelbas  22386  mdetdiaglem  22513  mdetralt2  22524  mndifsplit  22551  smadiadetglem2  22587  1elcpmat  22630  pmatcollpw3lem  22698  chfacfisf  22769  chfacfisfcpmat  22770  chfacffsupp  22771  chfacfscmulfsupp  22774  chfacfscmulgsum  22775  chfacfpmmulfsupp  22778  chfacfpmmulgsum  22779  chfacfpmmulgsum2  22780  cayhamlem1  22781  cpmadugsumlemF  22791  cayleyhamilton1  22807  tgcl  22884  pptbas  22923  clsval2  22965  mretopd  23007  lmbr2  23174  cncls2  23188  nrmsep  23272  regsep2  23291  cmpsublem  23314  cmpsub  23315  tgcmp  23316  uncmp  23318  hauscmplem  23321  iunconnlem  23342  1stcrest  23368  2ndcctbss  23370  2ndcsep  23374  dis2ndc  23375  hausllycmp  23409  dislly  23412  kgentopon  23453  1stckgen  23469  kgencn3  23473  ptpjpre1  23486  ptbasin  23492  ptpjopn  23527  dfac14  23533  ptcnplem  23536  txcn  23541  txindis  23549  txdis1cn  23550  ptrescn  23554  txcmplem1  23556  txcmp  23558  txhaus  23562  txlm  23563  tx1stc  23565  txkgen  23567  xkococn  23575  qtopcn  23629  kqreglem1  23656  kqreglem2  23657  kqnrmlem1  23658  kqnrmlem2  23659  hmeoimaf1o  23685  reghmph  23708  nrmhmph  23709  txhmeo  23718  ptuncnv  23722  filconn  23798  fbasrn  23799  fmfnfmlem2  23870  flimfnfcls  23943  cnpfcfi  23955  alexsublem  23959  alexsubALTlem2  23963  alexsubALTlem3  23964  alexsubALTlem4  23965  alexsubALT  23966  ptcmplem3  23969  cnextfval  23977  tsmsxp  24070  imasdsf1olem  24288  bl2in  24315  blssps  24339  blss  24340  blssexps  24341  blssex  24342  blcld  24420  stdbdxmet  24430  met1stc  24436  prdsxmslem2  24444  metcnp3  24455  metcnpi3  24461  txmetcnp  24462  nmo0  24650  nmoid  24657  icccmplem1  24738  icccmp  24741  xrge0tsms  24750  metdseq0  24770  cnheiborlem  24880  cnheibor  24881  cnllycmp  24882  pcoval2  24943  cmetcaulem  25215  iscmet3lem1  25218  iscmet3lem2  25219  equivcau  25227  lmcau  25240  cncmet  25249  ivthlem2  25380  ivthlem3  25381  ovoliunlem2  25431  ovolscalem2  25442  uniioombl  25517  dyaddisj  25524  opnmbllem  25529  volivth  25535  ismbfd  25567  ismbf3d  25582  mbfimaopnlem  25583  mbfinf  25593  itg1addlem4  25627  mbfi1fseqlem1  25643  mbfi1fseqlem3  25645  mbfi1fseqlem4  25646  mbfi1fseqlem5  25647  mbfi1fseqlem6  25648  itg2seq  25670  itg2lea  25672  itg2split  25677  itg2cnlem1  25689  bddiblnc  25770  limciun  25822  dvmptfsum  25906  rolle  25921  c1lip1  25929  dvcnvrelem1  25949  dvcnvre  25951  dvcvx  25952  itgsubst  25983  tdeglem4  25992  mdegmullem  26010  plyco0  26124  coemullem  26182  dgreq0  26198  dgrmul  26203  dgrco  26208  elqaalem2  26255  aannenlem1  26263  aaliou3lem9  26285  ulmres  26324  ulmshftlem  26325  angneg  26740  dcubic  26783  cxploglim  26915  cxploglim2  26916  scvxcvx  26923  lgamgulmlem5  26970  lgamcvg2  26992  ftalem2  27011  basellem3  27020  basellem4  27021  sqff1o  27119  fsumdvdsdiaglem  27120  dvdsflsumcom  27125  mpodvdsmulf1o  27131  dvdsmulf1o  27133  fsumvma2  27152  logfac2  27155  logfacrlim  27162  logexprlim  27163  dchrelbasd  27177  lgsne0  27273  lgsqrlem2  27285  lgsqrmodndvds  27291  gausslemma2dlem1a  27303  lgseisenlem2  27314  lgsquadlem1  27318  lgsquadlem2  27319  lgsquadlem3  27320  lgsquad2lem2  27323  2sqlem8  27364  2sqlem11  27367  2sqreultlem  27385  2sqreunnltlem  27388  chpo1ubb  27419  vmadivsum  27420  rplogsumlem2  27423  rpvmasumlem  27425  dchrmusum2  27432  dchrvmasumlem1  27433  dchrisum0fno1  27449  dchrisum0re  27451  dchrisum0lem1  27454  dchrisum0lem2  27456  dchrisum0lem3  27457  dchrisum0  27458  mulogsumlem  27469  mulog2sumlem2  27473  vmalogdivsum2  27476  logsqvma  27480  log2sumbnd  27482  selberglem3  27485  selberg  27486  selberg2lem  27488  selberg2b  27490  selberg3lem2  27496  pntrmax  27502  pntrsumo1  27503  pntlemn  27538  pntlemp  27548  qabvle  27563  ostthlem1  27565  ostthlem2  27566  ostth2lem2  27572  ostth3  27576  sltres  27601  nosupno  27642  nosupbnd2  27655  noinfno  27657  noinfbnd2  27670  etasslt  27754  cuteq1  27778  addsproplem2  27913  mulsval  28048  precsexlem11  28155  n0sfincut  28282  zmulscld  28321  idmot  28515  brbtwn2  28883  colinearalglem4  28887  colinearalg  28888  ax5seglem9  28915  axpaschlem  28918  axcontlem2  28943  axcontlem7  28948  axcontlem8  28949  eengtrkg  28964  upgr1eopALT  29095  uspgredg2vlem  29201  subumgr  29266  nbgr0edglem  29334  edgnbusgreu  29345  nb3grprlem1  29358  wlkl1loop  29616  pthdivtx  29705  usgr2pth  29742  crctcshwlkn0  29799  wlklnwwlkln1  29846  wwlksnext  29871  clwwlkccatlem  29969  clwlkclwwlklem2a  29978  clwwlkinwwlk  30020  clwwlkn1loopb  30023  clwwlkf  30027  wwlksext2clwwlk  30037  wwlksubclwwlk  30038  clwwlknscsh  30042  clwwlknon1  30077  clwwlknonex2e  30090  1conngr  30174  n4cyclfrgr  30271  numclwwlk2lem1lem  30322  2clwwlk2clwwlk  30330  numclwwlk1lem2f1  30337  numclwlk1lem1  30349  numclwwlk2lem1  30356  numclwlk2lem2f  30357  numclwwlk7  30371  frgrogt3nreg  30377  grpoidinvlem1  30484  grpoidinvlem3  30486  grporcan  30498  nmlnoubi  30776  blocnilem  30784  ipblnfi  30835  htthlem  30897  ocsh  31263  shmodsi  31369  pjhthlem2  31372  5oalem2  31635  eigposi  31816  nmopub2tALT  31889  nmfnleub2  31906  nmcexi  32006  nmopcoi  32075  kbass3  32098  mdslmd1lem1  32305  mdslmd1lem2  32306  chirredlem2  32371  chirredlem4  32373  mdsymlem3  32385  mdsymlem5  32387  sumdmdii  32395  sumdmdlem  32398  sumdmdlem2  32399  foresf1o  32484  disjxpin  32568  1stpreimas  32687  resf1o  32713  nn0xmulclb  32754  wrdt2ind  32934  xrge0tsmsd  33042  gsumvsca1  33195  gsumvsca2  33196  islinds5  33332  1arithidomlem2  33501  mplvrpmmhm  33576  irngnzply1  33704  mdetpmtr1  33836  mdetpmtr2  33837  pstmxmet  33910  qqhghm  34001  qqhrhm  34002  esumpcvgval  34091  volmeas  34244  imambfm  34275  dya2iocnrect  34294  oddpwdc  34367  sseqf  34405  orvcgteel  34481  orvclteel  34486  ballotlemsf1o  34527  bnj1110  34994  bnj1118  34996  f1resveqaeq  35097  txpconn  35276  connpconn  35279  cnllysconn  35289  rellysconn  35295  cvmsss2  35318  cvmlift2lem9  35355  satf00  35418  fmlasuc  35430  mrsubfval  35552  mppsval  35616  dfon2lem6  35830  wzel  35866  ifscgr  36088  cgrxfr  36099  btwnconn1lem5  36135  btwnconn1lem6  36136  btwnconn1lem12  36142  brsegle  36152  finminlem  36362  nn0prpwlem  36366  fnessref  36401  refssfne  36402  neibastop1  36403  topjoin  36409  fnemeet2  36411  weiunse  36512  bj-prmoore  37159  bj-finsumval0  37329  topdifinffinlem  37391  lindsadd  37663  matunitlindflem2  37667  poimirlem28  37698  poimirlem32  37702  opnmbllem0  37706  mblfinlem1  37707  mblfinlem4  37710  ismblfin  37711  mbfresfi  37716  itg2addnclem  37721  itg2addnclem3  37723  itg2addnc  37724  unirep  37764  frinfm  37785  sdclem2  37792  geomcau  37809  istotbnd3  37821  sstotbnd2  37824  sstotbnd  37825  sstotbnd3  37826  totbndbnd  37839  cntotbnd  37846  ismtyres  37858  heibor1lem  37859  heiborlem1  37861  heiborlem8  37868  ismndo1  37923  isdivrngo  38000  unichnidl  38081  erimeq2  38786  cvlcvr1  39448  ishlat3N  39463  llnmlplnN  39648  islvol2aN  39701  4atlem4c  39710  4atlem4d  39711  isline2  39883  isline3  39885  linepsubclN  40060  lhpexle3lem  40120  lhpjat2  40130  cdlemd4  40310  cdleme0cq  40324  cdleme32fva  40546  cdleme32fvaw  40548  tendo0mul  40935  tendo0mulr  40936  diameetN  41165  dvhvaddcl  41204  dvhvaddcomN  41205  cdlemm10N  41227  dvadiaN  41237  djavalN  41244  dihvalcqat  41348  dihopelvalcpre  41357  djhval  41507  dihjat1lem  41537  sticksstones11  42259  sticksstones22  42271  f1o2d2  42336  remul01  42510  zaddcom  42567  zmulcom  42571  fidomncyc  42638  evlselvlem  42689  evlselv  42690  fsuppind  42693  mhpind  42697  prjspertr  42708  prjsprellsp  42714  elrfi  42797  nacsfix  42815  fzsplit1nn0  42857  eldioph2  42865  lzenom  42873  irrapxlem3  42927  pellexlem5  42936  pell1234qrne0  42956  pell1234qrmulcl  42958  pell14qrdich  42972  pell1qrge1  42973  pellqrex  42982  reglogltb  42994  reglogleb  42995  rmxypairf1o  43014  rmxycomplete  43020  monotoddzzfi  43045  congadd  43069  congsym  43071  acongrep  43083  jm2.19lem3  43094  jm2.19lem4  43095  jm2.22  43098  jm2.25  43102  expdiophlem1  43124  wepwsolem  43145  kelac1  43166  lmhmfgsplit  43189  pwslnm  43197  hbtlem6  43232  hbt  43233  mon1psubm  43302  deg1mhm  43303  omord2lim  43403  succlg  43431  onmcl  43434  ofoafo  43459  ofoacom  43464  fzunt  43558  fzuntd  43559  fzunt1d  43560  fzuntgd  43561  iunrelexp0  43805  dssmapnvod  44123  gsumws3  44299  gsumws4  44300  mulltgt0  45129  fnchoice  45136  disjrnmpt2  45295  fzisoeu  45411  fsumiunss  45685  climinf  45716  mullimc  45726  mullimcf  45733  stoweidlem14  46122  stoweidlem17  46125  stoweidlem34  46142  stoweidlem50  46158  fourierdlem42  46257  fourierdlem62  46276  fourierdlem71  46285  fourierdlem76  46290  qndenserrnbllem  46402  subsaliuncl  46466  sge0resplit  46514  3f1oss1  47185  2reu8i  47223  addmodne  47454  fundcmpsurinjpreimafv  47518  iccpartigtl  47533  prproropf1olem2  47614  prproropf1olem4  47616  paireqne  47621  prmdvdsfmtnof1lem2  47695  bgoldbtbndlem3  47917  bgoldbtbnd  47919  grimcnv  47998  gricushgr  48027  cycldlenngric  48038  grimedg  48045  grtrimap  48058  isubgr3stgrlem6  48081  isubgr3stgrlem7  48082  isubgr3stgrlem8  48083  isubgr3stgrlem9  48084  grlimfn  48089  gpgedg2iv  48177  gpg5nbgrvtx03starlem2  48179  gpg5nbgrvtx13starlem2  48182  uspgrsprf1  48257  isassintop  48320  2zlidl  48350  2zrngnmrid  48366  rngcinvALTV  48386  funcringcsetcALTV2lem9  48408  ringcinvALTV  48420  funcringcsetclem9ALTV  48431  fldhmsubcALTV  48443  gsumlsscl  48490  lincsum  48540  lindslinindsimp1  48568  lindslinindimp2lem4  48572  lincresunitlem2  48587  elfzolborelfzop1  48630  elbigo2  48663  digexp  48718  dig1  48719  nn0sumshdiglemB  48731  1arymaptf1  48753  2arymaptf1  48764  itcoval1  48774  itcoval2  48775  itcoval3  48776  itcovalsucov  48779  ackvalsuc1mpt  48789  itschlc0xyqsol  48878  brab2dd  48938  dmrnxp  48947  xpco2  48967  initopropd  49354  termopropd  49355  zeroopropd  49356  prcofpropd  49490  thincciso  49564  indthinc  49573  indthincALT  49574  oduoppcciso  49677  lanpropd  49726  ranpropd  49727