Theorem ad2antrl 729

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 718	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  771  simprll  779  simprlr  780  simprl1  1220  simprl2  1221  simprl3  1222  disjxiun  5083  reusv2lem4  5340  axprlem5OLD  5370  fr2nr  5603  somin1  6092  tz7.7  6345  f1oprg  6822  soisores  7277  elovmporab1w  7609  elovmporab1  7610  sorpssi  7678  onint  7739  ordsucelsuc  7768  elxp5  7869  resf1extb  7880  f1oabexg  7888  wemoiso  7921  wemoiso2  7922  el2xptp0  7984  frxp2  8089  frxp3  8096  ressuppss  8128  fprlem1  8245  tz7.48lem  8375  oalimcl  8490  oeeui  8533  nnaordex2  8570  oaabs2  8580  omabs  8582  swoer  8670  ralxpmap  8839  pw2f1olem  9014  enfixsn  9019  mapxpen  9076  mapunen  9079  php  9136  unxpdomlem2  9162  unxpdomlem3  9163  isfinite2  9203  fodomfi  9217  domunfican  9227  fodomfiOLD  9235  fissuni  9262  fipreima  9263  indexfi  9265  fsuppsssupp  9289  marypha1lem  9341  marypha2  9347  supmo  9360  infmo  9405  oieu  9449  brwdom2  9483  ixpiunwdom  9500  cantnfval2  9585  cantnfle  9587  cantnflt  9588  cantnf  9609  wemapwe  9613  cnfcom  9616  frrlem15  9676  rankonidlem  9747  r1pwcl  9766  eldju2ndl  9843  eldju2ndr  9844  djuun  9845  infxpenlem  9930  infxpenc2lem1  9936  fseqenlem1  9941  dfac8clem  9949  mappwen  10029  dfac3  10038  dfac5  10046  dfac12lem3  10063  infunsdom  10130  coftr  10190  ssfin4  10227  domfin4  10228  fin23lem26  10242  fin23lem22  10244  fin23lem28  10257  fin23lem32  10261  fin23lem40  10268  isf32lem5  10274  compssiso  10291  isf34lem4  10294  isfin1-3  10303  fin1a2lem13  10329  hsmexlem2  10344  hsmexlem4  10346  zorn2lem1  10413  ttukeylem6  10431  iundom2g  10457  konigthlem  10486  pwcfsdom  10501  fpwwe2lem11  10559  fpwwe2  10561  pwfseqlem3  10578  winalim2  10614  r1wunlim  10655  inttsk  10692  inar1  10693  grur1  10738  nqereq  10853  ltexprlem7  10960  prlem936  10965  00id  11316  addlid  11324  ltord1  11671  divdiv1  11861  divdiv2  11862  conjmul  11867  ltdivmul  12026  ledivmul  12027  lt2mul2div  12029  ltdiv23  12042  lediv23  12043  lediv12a  12044  ledivp1  12053  negfi  12100  nn0nndivcl  12504  nn0ge0div  12593  peano2uz2  12612  peano5uzi  12613  eluzp1m1  12809  qbtwnre  13146  xralrple  13152  xleadd1a  13200  xmulge0  13231  xmulass  13234  xlemul1a  13235  iooshf  13374  divelunit  13442  eluzgtdifelfzo  13677  modadd1  13862  modmul1  13881  seqcl2  13977  seqfveq2  13981  seqid2  14005  seqhomo  14006  seqdistr  14010  mulexpz  14059  leexp2r  14131  expnlbnd2  14191  expmulnbnd  14192  hashmap  14392  hashfun  14394  hashbclem  14409  hashfacen  14411  hashf1lem2  14413  hashf1  14414  ccatsymb  14540  swrdwrdsymb  14620  swrdsb0eq  14621  ccatpfx  14658  swrdswrd  14662  wrdind  14679  wrd2ind  14680  swrdccatin1  14682  swrdccatin2  14686  pfxccatin12lem2  14688  pfxccatin12  14690  swrdccat  14692  repswswrd  14741  0csh0  14750  cshwidxmod  14760  2cshw  14770  cshweqrep  14778  relexp0g  14979  relexpsucnnr  14982  relexpindlem  15020  01sqrexlem1  15199  01sqrexlem6  15204  rlim  15452  rlimclim1  15502  climsup  15627  caurcvg2  15635  caucvgb  15637  iseralt  15642  sumss  15681  fsum2dlem  15727  mptfzshft  15735  modfsummod  15752  o1fsum  15771  incexclem  15796  divrcnv  15812  flo1  15814  fprodrev  15937  fprod2dlem  15940  ruclem6  16197  moddvds  16227  dvdsaddre2b  16271  dvdsflip  16281  addmodlteqALT  16289  nn0o  16347  fldivndvdslt  16380  bitsf1ocnv  16408  bitsf1  16410  sadcaddlem  16421  bezoutlem2  16504  bezoutlem4  16506  lcmgcdlem  16570  prmind2  16649  isprm5  16672  isprm6  16679  prmdvdsncoprmbd  16692  cncongrprm  16694  hashdvds  16740  crth  16743  eulerthlem2  16747  prmdiveq  16751  hashgcdlem  16753  hashgcdeq  16755  iserodd  16801  pclem  16804  pcprendvds2  16807  pcexp  16825  pcneg  16840  pc2dvds  16845  pcmpt  16858  prmpwdvds  16870  pockthg  16872  prmreclem5  16886  4sqlem11  16921  ramub2  16980  ramubcl  16984  ram0  16988  ramub1lem2  16993  ramcl  16995  prmgaplem3  17019  prmgaplem6  17022  setscom  17145  sscpwex  17777  initoeu2  17978  setcinv  18052  funcestrcsetclem9  18109  funcsetcestrclem9  18124  fullsetcestrc  18127  1stfcl  18158  2ndfcl  18159  hofpropd  18228  isacs3lem  18503  isacs4lem  18505  acsmap2d  18516  chnflenfi  18589  subsubmgm  18673  submnd0  18726  mndpsuppss  18728  subsubm  18779  insubm  18781  frmdup1  18827  frmdup3lem  18829  sgrp2nmndlem2  18890  isgrpinv  18964  subsubg  19120  cycsubgcl  19176  conjghm  19219  qusghm  19225  gsumwrev  19336  gsmsymgrfixlem1  19397  symgfixelsi  19405  symgsssg  19437  symgfisg  19438  psgnunilem2  19465  odf1o2  19543  sylow1lem1  19568  odcau  19574  pgpfi  19575  pgpssslw  19584  fislw  19595  efgtlen  19696  efginvrel2  19697  efgrelexlemb  19720  efgredeu  19722  efgcpbllemb  19725  frgpup1  19745  lt6abl  19865  gsum2d  19942  gsum2d2lem  19943  gsum2d2  19944  telgsumfzslem  19958  dmdprdsplit2lem  20017  ablfacrp  20038  pgpfac1lem3  20049  gsummgp0  20292  irredrmul  20402  subsubrng  20535  subsubrg  20570  rngcinv  20609  ringcinv  20643  fldhmsubc  20757  islss4  20952  lspextmo  21047  lspsnat  21139  prmirredlem  21466  znf1o  21545  znidomb  21555  frgpcyg  21567  psgnghm  21574  psgndiflemB  21594  frlmlbs  21791  frlmup1  21792  lindfind  21810  islindf3  21820  lindfmm  21821  issubassa3  21860  resspsradd  21967  resspsrmul  21968  psdmul  22146  coe1tmmul2  22255  pf1ind  22334  mamulid  22420  mat1dimelbas  22450  mdetdiaglem  22577  mdetralt2  22588  mndifsplit  22615  smadiadetglem2  22651  1elcpmat  22694  pmatcollpw3lem  22762  chfacfisf  22833  chfacfisfcpmat  22834  chfacffsupp  22835  chfacfscmulfsupp  22838  chfacfscmulgsum  22839  chfacfpmmulfsupp  22842  chfacfpmmulgsum  22843  chfacfpmmulgsum2  22844  cayhamlem1  22845  cpmadugsumlemF  22855  cayleyhamilton1  22871  tgcl  22948  pptbas  22987  clsval2  23029  mretopd  23071  lmbr2  23238  cncls2  23252  nrmsep  23336  regsep2  23355  cmpsublem  23378  cmpsub  23379  tgcmp  23380  uncmp  23382  hauscmplem  23385  iunconnlem  23406  1stcrest  23432  2ndcctbss  23434  2ndcsep  23438  dis2ndc  23439  hausllycmp  23473  dislly  23476  kgentopon  23517  1stckgen  23533  kgencn3  23537  ptpjpre1  23550  ptbasin  23556  ptpjopn  23591  dfac14  23597  ptcnplem  23600  txcn  23605  txindis  23613  txdis1cn  23614  ptrescn  23618  txcmplem1  23620  txcmp  23622  txhaus  23626  txlm  23627  tx1stc  23629  txkgen  23631  xkococn  23639  qtopcn  23693  kqreglem1  23720  kqreglem2  23721  kqnrmlem1  23722  kqnrmlem2  23723  hmeoimaf1o  23749  reghmph  23772  nrmhmph  23773  txhmeo  23782  ptuncnv  23786  filconn  23862  fbasrn  23863  fmfnfmlem2  23934  flimfnfcls  24007  cnpfcfi  24019  alexsublem  24023  alexsubALTlem2  24027  alexsubALTlem3  24028  alexsubALTlem4  24029  alexsubALT  24030  ptcmplem3  24033  cnextfval  24041  tsmsxp  24134  imasdsf1olem  24352  bl2in  24379  blssps  24403  blss  24404  blssexps  24405  blssex  24406  blcld  24484  stdbdxmet  24494  met1stc  24500  prdsxmslem2  24508  metcnp3  24519  metcnpi3  24525  txmetcnp  24526  nmo0  24714  nmoid  24721  icccmplem1  24802  icccmp  24805  xrge0tsms  24814  metdseq0  24834  cnheiborlem  24935  cnheibor  24936  cnllycmp  24937  pcoval2  24997  cmetcaulem  25269  iscmet3lem1  25272  iscmet3lem2  25273  equivcau  25281  lmcau  25294  cncmet  25303  ivthlem2  25433  ivthlem3  25434  ovoliunlem2  25484  ovolscalem2  25495  uniioombl  25570  dyaddisj  25577  opnmbllem  25582  volivth  25588  ismbfd  25620  ismbf3d  25635  mbfimaopnlem  25636  mbfinf  25646  itg1addlem4  25680  mbfi1fseqlem1  25696  mbfi1fseqlem3  25698  mbfi1fseqlem4  25699  mbfi1fseqlem5  25700  mbfi1fseqlem6  25701  itg2seq  25723  itg2lea  25725  itg2split  25730  itg2cnlem1  25742  bddiblnc  25823  limciun  25875  dvmptfsum  25956  rolle  25971  c1lip1  25978  dvcnvrelem1  25998  dvcnvre  26000  dvcvx  26001  itgsubst  26030  tdeglem4  26039  mdegmullem  26057  plyco0  26171  coemullem  26229  dgreq0  26244  dgrmul  26249  dgrco  26254  elqaalem2  26301  aannenlem1  26309  aaliou3lem9  26331  ulmres  26370  ulmshftlem  26371  angneg  26784  dcubic  26827  cxploglim  26959  cxploglim2  26960  scvxcvx  26967  lgamgulmlem5  27014  lgamcvg2  27036  ftalem2  27055  basellem3  27064  basellem4  27065  sqff1o  27163  fsumdvdsdiaglem  27164  dvdsflsumcom  27169  mpodvdsmulf1o  27175  dvdsmulf1o  27177  fsumvma2  27195  logfac2  27198  logfacrlim  27205  logexprlim  27206  dchrelbasd  27220  lgsne0  27316  lgsqrlem2  27328  lgsqrmodndvds  27334  gausslemma2dlem1a  27346  lgseisenlem2  27357  lgsquadlem1  27361  lgsquadlem2  27362  lgsquadlem3  27363  lgsquad2lem2  27366  2sqlem8  27407  2sqlem11  27410  2sqreultlem  27428  2sqreunnltlem  27431  chpo1ubb  27462  vmadivsum  27463  rplogsumlem2  27466  rpvmasumlem  27468  dchrmusum2  27475  dchrvmasumlem1  27476  dchrisum0fno1  27492  dchrisum0re  27494  dchrisum0lem1  27497  dchrisum0lem2  27499  dchrisum0lem3  27500  dchrisum0  27501  mulogsumlem  27512  mulog2sumlem2  27516  vmalogdivsum2  27519  logsqvma  27523  log2sumbnd  27525  selberglem3  27528  selberg  27529  selberg2lem  27531  selberg2b  27533  selberg3lem2  27539  pntrmax  27545  pntrsumo1  27546  pntlemn  27581  pntlemp  27591  qabvle  27606  ostthlem1  27608  ostthlem2  27609  ostth2lem2  27615  ostth3  27619  ltsres  27644  nosupno  27685  nosupbnd2  27698  noinfno  27700  noinfbnd2  27713  etaslts  27803  cuteq1  27827  addsproplem2  27980  mulsval  28119  precsexlem11  28227  n0fincut  28365  zmulscld  28407  bdayfinbndlem1  28477  idmot  28623  brbtwn2  28992  colinearalglem4  28996  colinearalg  28997  ax5seglem9  29024  axpaschlem  29027  axcontlem2  29052  axcontlem7  29057  axcontlem8  29058  eengtrkg  29073  upgr1eopALT  29204  uspgredg2vlem  29310  subumgr  29375  nbgr0edglem  29443  edgnbusgreu  29454  nb3grprlem1  29467  wlkl1loop  29725  pthdivtx  29814  usgr2pth  29851  crctcshwlkn0  29908  wlklnwwlkln1  29955  wwlksnext  29980  clwwlkccatlem  30078  clwlkclwwlklem2a  30087  clwwlkinwwlk  30129  clwwlkn1loopb  30132  clwwlkf  30136  wwlksext2clwwlk  30146  wwlksubclwwlk  30147  clwwlknscsh  30151  clwwlknon1  30186  clwwlknonex2e  30199  1conngr  30283  n4cyclfrgr  30380  numclwwlk2lem1lem  30431  2clwwlk2clwwlk  30439  numclwwlk1lem2f1  30446  numclwlk1lem1  30458  numclwwlk2lem1  30465  numclwlk2lem2f  30466  numclwwlk7  30480  frgrogt3nreg  30486  grpoidinvlem1  30594  grpoidinvlem3  30596  grporcan  30608  nmlnoubi  30886  blocnilem  30894  ipblnfi  30945  htthlem  31007  ocsh  31373  shmodsi  31479  pjhthlem2  31482  5oalem2  31745  eigposi  31926  nmopub2tALT  31999  nmfnleub2  32016  nmcexi  32116  nmopcoi  32185  kbass3  32208  mdslmd1lem1  32415  mdslmd1lem2  32416  chirredlem2  32481  chirredlem4  32483  mdsymlem3  32495  mdsymlem5  32497  sumdmdii  32505  sumdmdlem  32508  sumdmdlem2  32509  foresf1o  32593  disjxpin  32677  1stpreimas  32798  resf1o  32822  nn0xmulclb  32863  wrdt2ind  33032  xrge0tsmsd  33153  gsumvsca1  33306  gsumvsca2  33307  islinds5  33446  1arithidomlem2  33615  mplvrpmmhm  33709  irngnzply1  33855  mdetpmtr1  33987  mdetpmtr2  33988  pstmxmet  34061  qqhghm  34152  qqhrhm  34153  esumpcvgval  34242  volmeas  34395  imambfm  34426  dya2iocnrect  34445  oddpwdc  34518  sseqf  34556  orvcgteel  34632  orvclteel  34637  ballotlemsf1o  34678  bnj1110  35144  bnj1118  35146  f1resveqaeq  35248  txpconn  35434  connpconn  35437  cnllysconn  35447  rellysconn  35453  cvmsss2  35476  cvmlift2lem9  35513  satf00  35576  fmlasuc  35588  mrsubfval  35710  mppsval  35774  dfon2lem6  35988  wzel  36024  ifscgr  36246  cgrxfr  36257  btwnconn1lem5  36293  btwnconn1lem6  36294  btwnconn1lem12  36300  brsegle  36310  finminlem  36520  nn0prpwlem  36524  fnessref  36559  refssfne  36560  neibastop1  36561  topjoin  36567  fnemeet2  36569  weiunse  36670  mh-inf3f1  36743  bj-prmoore  37447  bj-finsumval0  37619  topdifinffinlem  37681  lindsadd  37952  matunitlindflem2  37956  poimirlem28  37987  poimirlem32  37991  opnmbllem0  37995  mblfinlem1  37996  mblfinlem4  37999  ismblfin  38000  mbfresfi  38005  itg2addnclem  38010  itg2addnclem3  38012  itg2addnc  38013  unirep  38053  frinfm  38074  sdclem2  38081  geomcau  38098  istotbnd3  38110  sstotbnd2  38113  sstotbnd  38114  sstotbnd3  38115  totbndbnd  38128  cntotbnd  38135  ismtyres  38147  heibor1lem  38148  heiborlem1  38150  heiborlem8  38157  ismndo1  38212  isdivrngo  38289  unichnidl  38370  erimeq2  39102  cvlcvr1  39803  ishlat3N  39818  llnmlplnN  40003  islvol2aN  40056  4atlem4c  40065  4atlem4d  40066  isline2  40238  isline3  40240  linepsubclN  40415  lhpexle3lem  40475  lhpjat2  40485  cdlemd4  40665  cdleme0cq  40679  cdleme32fva  40901  cdleme32fvaw  40903  tendo0mul  41290  tendo0mulr  41291  diameetN  41520  dvhvaddcl  41559  dvhvaddcomN  41560  cdlemm10N  41582  dvadiaN  41592  djavalN  41599  dihvalcqat  41703  dihopelvalcpre  41712  djhval  41862  dihjat1lem  41892  sticksstones11  42613  sticksstones22  42625  f1o2d2  42692  remul01  42857  zaddcom  42927  zmulcom  42931  fidomncyc  42998  evlselvlem  43037  evlselv  43038  fsuppind  43041  mhpind  43045  prjspertr  43056  prjsprellsp  43062  elrfi  43144  nacsfix  43162  fzsplit1nn0  43204  eldioph2  43212  lzenom  43220  irrapxlem3  43274  pellexlem5  43283  pell1234qrne0  43303  pell1234qrmulcl  43305  pell14qrdich  43319  pell1qrge1  43320  pellqrex  43329  reglogltb  43341  reglogleb  43342  rmxypairf1o  43361  rmxycomplete  43367  monotoddzzfi  43392  congadd  43416  congsym  43418  acongrep  43430  jm2.19lem3  43441  jm2.19lem4  43442  jm2.22  43445  jm2.25  43449  expdiophlem1  43471  wepwsolem  43492  kelac1  43513  lmhmfgsplit  43536  pwslnm  43544  hbtlem6  43579  hbt  43580  mon1psubm  43649  deg1mhm  43650  omord2lim  43750  succlg  43778  onmcl  43781  ofoafo  43806  ofoacom  43811  fzunt  43904  fzuntd  43905  fzunt1d  43906  fzuntgd  43907  iunrelexp0  44151  dssmapnvod  44469  gsumws3  44645  gsumws4  44646  mulltgt0  45475  fnchoice  45482  disjrnmpt2  45640  fzisoeu  45755  fsumiunss  46027  climinf  46058  mullimc  46068  mullimcf  46075  stoweidlem14  46464  stoweidlem17  46467  stoweidlem34  46484  stoweidlem50  46500  fourierdlem42  46599  fourierdlem62  46618  fourierdlem71  46627  fourierdlem76  46632  qndenserrnbllem  46744  subsaliuncl  46808  sge0resplit  46856  3f1oss1  47539  2reu8i  47577  addmodne  47814  fundcmpsurinjpreimafv  47884  iccpartigtl  47899  prproropf1olem2  47980  prproropf1olem4  47982  paireqne  47987  prmdvdsfmtnof1lem2  48064  nprmdvdsfacm1  48103  bgoldbtbndlem3  48299  bgoldbtbnd  48301  grimcnv  48380  gricushgr  48409  cycldlenngric  48420  grimedg  48427  grtrimap  48440  isubgr3stgrlem6  48463  isubgr3stgrlem7  48464  isubgr3stgrlem8  48465  isubgr3stgrlem9  48466  grlimfn  48471  gpgedg2iv  48559  gpg5nbgrvtx03starlem2  48561  gpg5nbgrvtx13starlem2  48564  uspgrsprf1  48639  isassintop  48702  2zlidl  48732  2zrngnmrid  48748  rngcinvALTV  48768  funcringcsetcALTV2lem9  48790  ringcinvALTV  48802  funcringcsetclem9ALTV  48813  fldhmsubcALTV  48825  gsumlsscl  48872  lincsum  48921  lindslinindsimp1  48949  lindslinindimp2lem4  48953  lincresunitlem2  48968  elfzolborelfzop1  49011  elbigo2  49044  digexp  49099  dig1  49100  nn0sumshdiglemB  49112  1arymaptf1  49134  2arymaptf1  49145  itcoval1  49155  itcoval2  49156  itcoval3  49157  itcovalsucov  49160  ackvalsuc1mpt  49170  itschlc0xyqsol  49259  brab2dd  49319  dmrnxp  49328  xpco2  49348  initopropd  49734  termopropd  49735  zeroopropd  49736  prcofpropd  49870  thincciso  49944  indthinc  49953  indthincALT  49954  oduoppcciso  50057  lanpropd  50106  ranpropd  50107