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  5095  reusv2lem4  5346  axprlem5OLD  5375  fr2nr  5601  somin1  6090  tz7.7  6343  f1oprg  6820  soisores  7273  elovmporab1w  7605  elovmporab1  7606  sorpssi  7674  onint  7735  ordsucelsuc  7764  elxp5  7865  resf1extb  7876  f1oabexg  7884  wemoiso  7917  wemoiso2  7918  el2xptp0  7980  frxp2  8086  frxp3  8093  ressuppss  8125  fprlem1  8242  tz7.48lem  8372  oalimcl  8487  oeeui  8530  nnaordex2  8567  oaabs2  8577  omabs  8579  swoer  8667  ralxpmap  8836  pw2f1olem  9011  enfixsn  9016  mapxpen  9073  mapunen  9076  php  9133  unxpdomlem2  9159  unxpdomlem3  9160  isfinite2  9200  fodomfi  9214  domunfican  9224  fodomfiOLD  9232  fissuni  9259  fipreima  9260  indexfi  9262  fsuppsssupp  9286  marypha1lem  9338  marypha2  9344  supmo  9357  infmo  9402  oieu  9446  brwdom2  9480  ixpiunwdom  9497  cantnfval2  9580  cantnfle  9582  cantnflt  9583  cantnf  9604  wemapwe  9608  cnfcom  9611  frrlem15  9671  rankonidlem  9742  r1pwcl  9761  eldju2ndl  9838  eldju2ndr  9839  djuun  9840  infxpenlem  9925  infxpenc2lem1  9931  fseqenlem1  9936  dfac8clem  9944  mappwen  10024  dfac3  10033  dfac5  10041  dfac12lem3  10058  infunsdom  10125  coftr  10185  ssfin4  10222  domfin4  10223  fin23lem26  10237  fin23lem22  10239  fin23lem28  10252  fin23lem32  10256  fin23lem40  10263  isf32lem5  10269  compssiso  10286  isf34lem4  10289  isfin1-3  10298  fin1a2lem13  10324  hsmexlem2  10339  hsmexlem4  10341  zorn2lem1  10408  ttukeylem6  10426  iundom2g  10452  konigthlem  10481  pwcfsdom  10496  fpwwe2lem11  10554  fpwwe2  10556  pwfseqlem3  10573  winalim2  10609  r1wunlim  10650  inttsk  10687  inar1  10688  grur1  10733  nqereq  10848  ltexprlem7  10955  prlem936  10960  00id  11310  addlid  11318  ltord1  11665  divdiv1  11854  divdiv2  11855  conjmul  11860  ltdivmul  12019  ledivmul  12020  lt2mul2div  12022  ltdiv23  12035  lediv23  12036  lediv12a  12037  ledivp1  12046  negfi  12093  nn0nndivcl  12475  nn0ge0div  12563  peano2uz2  12582  peano5uzi  12583  eluzp1m1  12779  qbtwnre  13116  xralrple  13122  xleadd1a  13170  xmulge0  13201  xmulass  13204  xlemul1a  13205  iooshf  13344  divelunit  13412  eluzgtdifelfzo  13645  modadd1  13830  modmul1  13849  seqcl2  13945  seqfveq2  13949  seqid2  13973  seqhomo  13974  seqdistr  13978  mulexpz  14027  leexp2r  14099  expnlbnd2  14159  expmulnbnd  14160  hashmap  14360  hashfun  14362  hashbclem  14377  hashfacen  14379  hashf1lem2  14381  hashf1  14382  ccatsymb  14508  swrdwrdsymb  14588  swrdsb0eq  14589  ccatpfx  14626  swrdswrd  14630  wrdind  14647  wrd2ind  14648  swrdccatin1  14650  swrdccatin2  14654  pfxccatin12lem2  14656  pfxccatin12  14658  swrdccat  14660  repswswrd  14709  0csh0  14718  cshwidxmod  14728  2cshw  14738  cshweqrep  14746  relexp0g  14947  relexpsucnnr  14950  relexpindlem  14988  01sqrexlem1  15167  01sqrexlem6  15172  rlim  15420  rlimclim1  15470  climsup  15595  caurcvg2  15603  caucvgb  15605  iseralt  15610  sumss  15649  fsum2dlem  15695  mptfzshft  15703  modfsummod  15719  o1fsum  15738  incexclem  15761  divrcnv  15777  flo1  15779  fprodrev  15902  fprod2dlem  15905  ruclem6  16162  moddvds  16192  dvdsaddre2b  16236  dvdsflip  16246  addmodlteqALT  16254  nn0o  16312  fldivndvdslt  16345  bitsf1ocnv  16373  bitsf1  16375  sadcaddlem  16386  bezoutlem2  16469  bezoutlem4  16471  lcmgcdlem  16535  prmind2  16614  isprm5  16636  isprm6  16643  prmdvdsncoprmbd  16656  cncongrprm  16658  hashdvds  16704  crth  16707  eulerthlem2  16711  prmdiveq  16715  hashgcdlem  16717  hashgcdeq  16719  iserodd  16765  pclem  16768  pcprendvds2  16771  pcexp  16789  pcneg  16804  pc2dvds  16809  pcmpt  16822  prmpwdvds  16834  pockthg  16836  prmreclem5  16850  4sqlem11  16885  ramub2  16944  ramubcl  16948  ram0  16952  ramub1lem2  16957  ramcl  16959  prmgaplem3  16983  prmgaplem6  16986  setscom  17109  sscpwex  17741  initoeu2  17942  setcinv  18016  funcestrcsetclem9  18073  funcsetcestrclem9  18088  fullsetcestrc  18091  1stfcl  18122  2ndfcl  18123  hofpropd  18192  isacs3lem  18467  isacs4lem  18469  acsmap2d  18480  chnflenfi  18553  subsubmgm  18637  submnd0  18690  mndpsuppss  18692  subsubm  18743  insubm  18745  frmdup1  18791  frmdup3lem  18793  sgrp2nmndlem2  18851  isgrpinv  18925  subsubg  19081  cycsubgcl  19137  conjghm  19180  qusghm  19186  gsumwrev  19297  gsmsymgrfixlem1  19358  symgfixelsi  19366  symgsssg  19398  symgfisg  19399  psgnunilem2  19426  odf1o2  19504  sylow1lem1  19529  odcau  19535  pgpfi  19536  pgpssslw  19545  fislw  19556  efgtlen  19657  efginvrel2  19658  efgrelexlemb  19681  efgredeu  19683  efgcpbllemb  19686  frgpup1  19706  lt6abl  19826  gsum2d  19903  gsum2d2lem  19904  gsum2d2  19905  telgsumfzslem  19919  dmdprdsplit2lem  19978  ablfacrp  19999  pgpfac1lem3  20010  gsummgp0  20255  irredrmul  20365  subsubrng  20498  subsubrg  20533  rngcinv  20572  ringcinv  20606  fldhmsubc  20720  islss4  20915  lspextmo  21010  lspsnat  21102  prmirredlem  21429  znf1o  21508  znidomb  21518  frgpcyg  21530  psgnghm  21537  psgndiflemB  21557  frlmlbs  21754  frlmup1  21755  lindfind  21773  islindf3  21783  lindfmm  21784  issubassa3  21823  resspsradd  21932  resspsrmul  21933  psdmul  22111  coe1tmmul2  22220  pf1ind  22301  mamulid  22387  mat1dimelbas  22417  mdetdiaglem  22544  mdetralt2  22555  mndifsplit  22582  smadiadetglem2  22618  1elcpmat  22661  pmatcollpw3lem  22729  chfacfisf  22800  chfacfisfcpmat  22801  chfacffsupp  22802  chfacfscmulfsupp  22805  chfacfscmulgsum  22806  chfacfpmmulfsupp  22809  chfacfpmmulgsum  22810  chfacfpmmulgsum2  22811  cayhamlem1  22812  cpmadugsumlemF  22822  cayleyhamilton1  22838  tgcl  22915  pptbas  22954  clsval2  22996  mretopd  23038  lmbr2  23205  cncls2  23219  nrmsep  23303  regsep2  23322  cmpsublem  23345  cmpsub  23346  tgcmp  23347  uncmp  23349  hauscmplem  23352  iunconnlem  23373  1stcrest  23399  2ndcctbss  23401  2ndcsep  23405  dis2ndc  23406  hausllycmp  23440  dislly  23443  kgentopon  23484  1stckgen  23500  kgencn3  23504  ptpjpre1  23517  ptbasin  23523  ptpjopn  23558  dfac14  23564  ptcnplem  23567  txcn  23572  txindis  23580  txdis1cn  23581  ptrescn  23585  txcmplem1  23587  txcmp  23589  txhaus  23593  txlm  23594  tx1stc  23596  txkgen  23598  xkococn  23606  qtopcn  23660  kqreglem1  23687  kqreglem2  23688  kqnrmlem1  23689  kqnrmlem2  23690  hmeoimaf1o  23716  reghmph  23739  nrmhmph  23740  txhmeo  23749  ptuncnv  23753  filconn  23829  fbasrn  23830  fmfnfmlem2  23901  flimfnfcls  23974  cnpfcfi  23986  alexsublem  23990  alexsubALTlem2  23994  alexsubALTlem3  23995  alexsubALTlem4  23996  alexsubALT  23997  ptcmplem3  24000  cnextfval  24008  tsmsxp  24101  imasdsf1olem  24319  bl2in  24346  blssps  24370  blss  24371  blssexps  24372  blssex  24373  blcld  24451  stdbdxmet  24461  met1stc  24467  prdsxmslem2  24475  metcnp3  24486  metcnpi3  24492  txmetcnp  24493  nmo0  24681  nmoid  24688  icccmplem1  24769  icccmp  24772  xrge0tsms  24781  metdseq0  24801  cnheiborlem  24911  cnheibor  24912  cnllycmp  24913  pcoval2  24974  cmetcaulem  25246  iscmet3lem1  25249  iscmet3lem2  25250  equivcau  25258  lmcau  25271  cncmet  25280  ivthlem2  25411  ivthlem3  25412  ovoliunlem2  25462  ovolscalem2  25473  uniioombl  25548  dyaddisj  25555  opnmbllem  25560  volivth  25566  ismbfd  25598  ismbf3d  25613  mbfimaopnlem  25614  mbfinf  25624  itg1addlem4  25658  mbfi1fseqlem1  25674  mbfi1fseqlem3  25676  mbfi1fseqlem4  25677  mbfi1fseqlem5  25678  mbfi1fseqlem6  25679  itg2seq  25701  itg2lea  25703  itg2split  25708  itg2cnlem1  25720  bddiblnc  25801  limciun  25853  dvmptfsum  25937  rolle  25952  c1lip1  25960  dvcnvrelem1  25980  dvcnvre  25982  dvcvx  25983  itgsubst  26014  tdeglem4  26023  mdegmullem  26041  plyco0  26155  coemullem  26213  dgreq0  26229  dgrmul  26234  dgrco  26239  elqaalem2  26286  aannenlem1  26294  aaliou3lem9  26316  ulmres  26355  ulmshftlem  26356  angneg  26771  dcubic  26814  cxploglim  26946  cxploglim2  26947  scvxcvx  26954  lgamgulmlem5  27001  lgamcvg2  27023  ftalem2  27042  basellem3  27051  basellem4  27052  sqff1o  27150  fsumdvdsdiaglem  27151  dvdsflsumcom  27156  mpodvdsmulf1o  27162  dvdsmulf1o  27164  fsumvma2  27183  logfac2  27186  logfacrlim  27193  logexprlim  27194  dchrelbasd  27208  lgsne0  27304  lgsqrlem2  27316  lgsqrmodndvds  27322  gausslemma2dlem1a  27334  lgseisenlem2  27345  lgsquadlem1  27349  lgsquadlem2  27350  lgsquadlem3  27351  lgsquad2lem2  27354  2sqlem8  27395  2sqlem11  27398  2sqreultlem  27416  2sqreunnltlem  27419  chpo1ubb  27450  vmadivsum  27451  rplogsumlem2  27454  rpvmasumlem  27456  dchrmusum2  27463  dchrvmasumlem1  27464  dchrisum0fno1  27480  dchrisum0re  27482  dchrisum0lem1  27485  dchrisum0lem2  27487  dchrisum0lem3  27488  dchrisum0  27489  mulogsumlem  27500  mulog2sumlem2  27504  vmalogdivsum2  27507  logsqvma  27511  log2sumbnd  27513  selberglem3  27516  selberg  27517  selberg2lem  27519  selberg2b  27521  selberg3lem2  27527  pntrmax  27533  pntrsumo1  27534  pntlemn  27569  pntlemp  27579  qabvle  27594  ostthlem1  27596  ostthlem2  27597  ostth2lem2  27603  ostth3  27607  ltsres  27632  nosupno  27673  nosupbnd2  27686  noinfno  27688  noinfbnd2  27701  etaslts  27791  cuteq1  27815  addsproplem2  27968  mulsval  28107  precsexlem11  28215  n0fincut  28353  zmulscld  28395  bdayfinbndlem1  28465  idmot  28611  brbtwn2  28980  colinearalglem4  28984  colinearalg  28985  ax5seglem9  29012  axpaschlem  29015  axcontlem2  29040  axcontlem7  29045  axcontlem8  29046  eengtrkg  29061  upgr1eopALT  29192  uspgredg2vlem  29298  subumgr  29363  nbgr0edglem  29431  edgnbusgreu  29442  nb3grprlem1  29455  wlkl1loop  29713  pthdivtx  29802  usgr2pth  29839  crctcshwlkn0  29896  wlklnwwlkln1  29943  wwlksnext  29968  clwwlkccatlem  30066  clwlkclwwlklem2a  30075  clwwlkinwwlk  30117  clwwlkn1loopb  30120  clwwlkf  30124  wwlksext2clwwlk  30134  wwlksubclwwlk  30135  clwwlknscsh  30139  clwwlknon1  30174  clwwlknonex2e  30187  1conngr  30271  n4cyclfrgr  30368  numclwwlk2lem1lem  30419  2clwwlk2clwwlk  30427  numclwwlk1lem2f1  30434  numclwlk1lem1  30446  numclwwlk2lem1  30453  numclwlk2lem2f  30454  numclwwlk7  30468  frgrogt3nreg  30474  grpoidinvlem1  30581  grpoidinvlem3  30583  grporcan  30595  nmlnoubi  30873  blocnilem  30881  ipblnfi  30932  htthlem  30994  ocsh  31360  shmodsi  31466  pjhthlem2  31469  5oalem2  31732  eigposi  31913  nmopub2tALT  31986  nmfnleub2  32003  nmcexi  32103  nmopcoi  32172  kbass3  32195  mdslmd1lem1  32402  mdslmd1lem2  32403  chirredlem2  32468  chirredlem4  32470  mdsymlem3  32482  mdsymlem5  32484  sumdmdii  32492  sumdmdlem  32495  sumdmdlem2  32496  foresf1o  32581  disjxpin  32665  1stpreimas  32787  resf1o  32811  nn0xmulclb  32853  wrdt2ind  33037  xrge0tsmsd  33157  gsumvsca1  33310  gsumvsca2  33311  islinds5  33450  1arithidomlem2  33619  mplvrpmmhm  33713  irngnzply1  33850  mdetpmtr1  33982  mdetpmtr2  33983  pstmxmet  34056  qqhghm  34147  qqhrhm  34148  esumpcvgval  34237  volmeas  34390  imambfm  34421  dya2iocnrect  34440  oddpwdc  34513  sseqf  34551  orvcgteel  34627  orvclteel  34632  ballotlemsf1o  34673  bnj1110  35140  bnj1118  35142  f1resveqaeq  35243  txpconn  35428  connpconn  35431  cnllysconn  35441  rellysconn  35447  cvmsss2  35470  cvmlift2lem9  35507  satf00  35570  fmlasuc  35582  mrsubfval  35704  mppsval  35768  dfon2lem6  35982  wzel  36018  ifscgr  36240  cgrxfr  36251  btwnconn1lem5  36287  btwnconn1lem6  36288  btwnconn1lem12  36294  brsegle  36304  finminlem  36514  nn0prpwlem  36518  fnessref  36553  refssfne  36554  neibastop1  36555  topjoin  36561  fnemeet2  36563  weiunse  36664  bj-prmoore  37322  bj-finsumval0  37492  topdifinffinlem  37554  lindsadd  37816  matunitlindflem2  37820  poimirlem28  37851  poimirlem32  37855  opnmbllem0  37859  mblfinlem1  37860  mblfinlem4  37863  ismblfin  37864  mbfresfi  37869  itg2addnclem  37874  itg2addnclem3  37876  itg2addnc  37877  unirep  37917  frinfm  37938  sdclem2  37945  geomcau  37962  istotbnd3  37974  sstotbnd2  37977  sstotbnd  37978  sstotbnd3  37979  totbndbnd  37992  cntotbnd  37999  ismtyres  38011  heibor1lem  38012  heiborlem1  38014  heiborlem8  38021  ismndo1  38076  isdivrngo  38153  unichnidl  38234  erimeq2  38959  cvlcvr1  39621  ishlat3N  39636  llnmlplnN  39821  islvol2aN  39874  4atlem4c  39883  4atlem4d  39884  isline2  40056  isline3  40058  linepsubclN  40233  lhpexle3lem  40293  lhpjat2  40303  cdlemd4  40483  cdleme0cq  40497  cdleme32fva  40719  cdleme32fvaw  40721  tendo0mul  41108  tendo0mulr  41109  diameetN  41338  dvhvaddcl  41377  dvhvaddcomN  41378  cdlemm10N  41400  dvadiaN  41410  djavalN  41417  dihvalcqat  41521  dihopelvalcpre  41530  djhval  41680  dihjat1lem  41710  sticksstones11  42432  sticksstones22  42444  f1o2d2  42511  remul01  42683  zaddcom  42740  zmulcom  42744  fidomncyc  42811  evlselvlem  42850  evlselv  42851  fsuppind  42854  mhpind  42858  prjspertr  42869  prjsprellsp  42875  elrfi  42957  nacsfix  42975  fzsplit1nn0  43017  eldioph2  43025  lzenom  43033  irrapxlem3  43087  pellexlem5  43096  pell1234qrne0  43116  pell1234qrmulcl  43118  pell14qrdich  43132  pell1qrge1  43133  pellqrex  43142  reglogltb  43154  reglogleb  43155  rmxypairf1o  43174  rmxycomplete  43180  monotoddzzfi  43205  congadd  43229  congsym  43231  acongrep  43243  jm2.19lem3  43254  jm2.19lem4  43255  jm2.22  43258  jm2.25  43262  expdiophlem1  43284  wepwsolem  43305  kelac1  43326  lmhmfgsplit  43349  pwslnm  43357  hbtlem6  43392  hbt  43393  mon1psubm  43462  deg1mhm  43463  omord2lim  43563  succlg  43591  onmcl  43594  ofoafo  43619  ofoacom  43624  fzunt  43717  fzuntd  43718  fzunt1d  43719  fzuntgd  43720  iunrelexp0  43964  dssmapnvod  44282  gsumws3  44458  gsumws4  44459  mulltgt0  45288  fnchoice  45295  disjrnmpt2  45453  fzisoeu  45569  fsumiunss  45842  climinf  45873  mullimc  45883  mullimcf  45890  stoweidlem14  46279  stoweidlem17  46282  stoweidlem34  46299  stoweidlem50  46315  fourierdlem42  46414  fourierdlem62  46433  fourierdlem71  46442  fourierdlem76  46447  qndenserrnbllem  46559  subsaliuncl  46623  sge0resplit  46671  3f1oss1  47342  2reu8i  47380  addmodne  47611  fundcmpsurinjpreimafv  47675  iccpartigtl  47690  prproropf1olem2  47771  prproropf1olem4  47773  paireqne  47778  prmdvdsfmtnof1lem2  47852  bgoldbtbndlem3  48074  bgoldbtbnd  48076  grimcnv  48155  gricushgr  48184  cycldlenngric  48195  grimedg  48202  grtrimap  48215  isubgr3stgrlem6  48238  isubgr3stgrlem7  48239  isubgr3stgrlem8  48240  isubgr3stgrlem9  48241  grlimfn  48246  gpgedg2iv  48334  gpg5nbgrvtx03starlem2  48336  gpg5nbgrvtx13starlem2  48339  uspgrsprf1  48414  isassintop  48477  2zlidl  48507  2zrngnmrid  48523  rngcinvALTV  48543  funcringcsetcALTV2lem9  48565  ringcinvALTV  48577  funcringcsetclem9ALTV  48588  fldhmsubcALTV  48600  gsumlsscl  48647  lincsum  48696  lindslinindsimp1  48724  lindslinindimp2lem4  48728  lincresunitlem2  48743  elfzolborelfzop1  48786  elbigo2  48819  digexp  48874  dig1  48875  nn0sumshdiglemB  48887  1arymaptf1  48909  2arymaptf1  48920  itcoval1  48930  itcoval2  48931  itcoval3  48932  itcovalsucov  48935  ackvalsuc1mpt  48945  itschlc0xyqsol  49034  brab2dd  49094  dmrnxp  49103  xpco2  49123  initopropd  49509  termopropd  49510  zeroopropd  49511  prcofpropd  49645  thincciso  49719  indthinc  49728  indthincALT  49729  oduoppcciso  49832  lanpropd  49881  ranpropd  49882