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

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  simprl  770  simprll  778  simprlr  779  simprl1  1219  simprl2  1220  simprl3  1221  disjxiun  5146  reusv2lem4  5400  axprlem5  5426  fr2nr  5655  somin1  6135  tz7.7  6391  f1oprg  6879  soisores  7324  elovmporab1w  7653  elovmporab1  7654  sorpssi  7719  onint  7778  ordsucelsuc  7810  elxp5  7914  wemoiso  7960  wemoiso2  7961  el2xptp0  8022  frxp2  8130  frxp3  8137  ressuppss  8168  fprlem1  8285  tz7.48lem  8441  oalimcl  8560  oeeui  8602  oaabs2  8648  omabs  8650  swoer  8733  ralxpmap  8890  pw2f1olem  9076  enfixsn  9081  mapxpen  9143  mapunen  9146  php  9210  unxpdomlem2  9251  unxpdomlem3  9252  findcard3OLD  9286  isfinite2  9301  domunfican  9320  fodomfi  9325  fissuni  9357  fipreima  9358  indexfi  9360  fsuppsssupp  9379  marypha1lem  9428  marypha2  9434  supmo  9447  infmo  9490  oieu  9534  brwdom2  9568  ixpiunwdom  9585  cantnfval2  9664  cantnfle  9666  cantnflt  9667  cantnf  9688  wemapwe  9692  cnfcom  9695  frrlem15  9752  rankonidlem  9823  r1pwcl  9842  eldju2ndl  9919  eldju2ndr  9920  djuun  9921  infxpenlem  10008  infxpenc2lem1  10014  fseqenlem1  10019  dfac8clem  10027  mappwen  10107  dfac3  10116  dfac5  10123  dfac12lem3  10140  infunsdom  10209  coftr  10268  ssfin4  10305  domfin4  10306  fin23lem26  10320  fin23lem22  10322  fin23lem28  10335  fin23lem32  10339  fin23lem40  10346  isf32lem5  10352  compssiso  10369  isf34lem4  10372  isfin1-3  10381  fin1a2lem13  10407  hsmexlem2  10422  hsmexlem4  10424  zorn2lem1  10491  ttukeylem6  10509  iundom2g  10535  konigthlem  10563  pwcfsdom  10578  fpwwe2lem11  10636  fpwwe2  10638  pwfseqlem3  10655  winalim2  10691  r1wunlim  10732  inttsk  10769  inar1  10770  grur1  10815  nqereq  10930  ltexprlem7  11037  prlem936  11042  00id  11389  addlid  11397  ltord1  11740  divdiv1  11925  divdiv2  11926  conjmul  11931  ltdivmul  12089  ledivmul  12090  lt2mul2div  12092  ltdiv23  12105  lediv23  12106  lediv12a  12107  ledivp1  12116  negfi  12163  nn0nndivcl  12543  nn0ge0div  12631  peano2uz2  12650  peano5uzi  12651  eluzp1m1  12848  qbtwnre  13178  xralrple  13184  xleadd1a  13232  xmulge0  13263  xmulass  13266  xlemul1a  13267  iooshf  13403  divelunit  13471  eluzgtdifelfzo  13694  modadd1  13873  modmul1  13889  seqcl2  13986  seqfveq2  13990  seqid2  14014  seqhomo  14015  seqdistr  14019  mulexpz  14068  leexp2r  14139  expnlbnd2  14197  expmulnbnd  14198  hashmap  14395  hashfun  14397  hashbclem  14411  hashfacen  14413  hashfacenOLD  14414  hashf1lem2  14417  hashf1  14418  ccatsymb  14532  swrdwrdsymb  14612  swrdsb0eq  14613  ccatpfx  14651  swrdswrd  14655  wrdind  14672  wrd2ind  14673  swrdccatin1  14675  swrdccatin2  14679  pfxccatin12lem2  14681  pfxccatin12  14683  swrdccat  14685  repswswrd  14734  0csh0  14743  cshwidxmod  14753  2cshw  14763  cshweqrep  14771  relexp0g  14969  relexpsucnnr  14972  relexpindlem  15010  01sqrexlem1  15189  01sqrexlem6  15194  rlim  15439  rlimclim1  15489  climsup  15616  caurcvg2  15624  caucvgb  15626  iseralt  15631  sumss  15670  fsum2dlem  15716  mptfzshft  15724  modfsummod  15740  o1fsum  15759  incexclem  15782  divrcnv  15798  flo1  15800  fprodrev  15921  fprod2dlem  15924  ruclem6  16178  moddvds  16208  dvdsaddre2b  16250  dvdsflip  16260  addmodlteqALT  16268  nn0o  16326  fldivndvdslt  16357  bitsf1ocnv  16385  bitsf1  16387  sadcaddlem  16398  bezoutlem2  16482  bezoutlem4  16484  lcmgcdlem  16543  prmind2  16622  isprm5  16644  isprm6  16651  prmdvdsncoprmbd  16663  cncongrprm  16665  hashdvds  16708  crth  16711  eulerthlem2  16715  prmdiveq  16719  hashgcdlem  16721  hashgcdeq  16722  iserodd  16768  pclem  16771  pcprendvds2  16774  pcexp  16792  pcneg  16807  pc2dvds  16812  pcmpt  16825  prmpwdvds  16837  pockthg  16839  prmreclem5  16853  4sqlem11  16888  ramub2  16947  ramubcl  16951  ram0  16955  ramub1lem2  16960  ramcl  16962  prmgaplem3  16986  prmgaplem6  16989  setscom  17113  sscpwex  17762  initoeu2  17966  setcinv  18040  funcestrcsetclem9  18100  funcsetcestrclem9  18115  fullsetcestrc  18118  1stfcl  18149  2ndfcl  18150  hofpropd  18220  isacs3lem  18495  isacs4lem  18497  acsmap2d  18508  submnd0  18654  subsubm  18697  insubm  18699  frmdup1  18745  frmdup3lem  18747  sgrp2nmndlem2  18805  isgrpinv  18878  subsubg  19029  cycsubgcl  19083  conjghm  19123  qusghm  19129  gsumwrev  19233  gsmsymgrfixlem1  19295  symgfixelsi  19303  symgsssg  19335  symgfisg  19336  psgnunilem2  19363  odf1o2  19441  sylow1lem1  19466  odcau  19472  pgpfi  19473  pgpssslw  19482  fislw  19493  efgtlen  19594  efginvrel2  19595  efgrelexlemb  19618  efgredeu  19620  efgcpbllemb  19623  frgpup1  19643  lt6abl  19763  gsum2d  19840  gsum2d2lem  19841  gsum2d2  19842  telgsumfzslem  19856  dmdprdsplit2lem  19915  ablfacrp  19936  pgpfac1lem3  19947  gsummgp0  20130  irredrmul  20241  subsubrg  20345  islss4  20573  lspextmo  20667  lspsnat  20758  prmirredlem  21042  znf1o  21107  znidomb  21117  frgpcyg  21129  psgnghm  21133  psgndiflemB  21153  frlmlbs  21352  frlmup1  21353  lindfind  21371  islindf3  21381  lindfmm  21382  issubassa3  21420  resspsradd  21536  resspsrmul  21537  coe1tmmul2  21798  pf1ind  21874  mamulid  21943  mat1dimelbas  21973  mdetdiaglem  22100  mdetralt2  22111  mndifsplit  22138  smadiadetglem2  22174  1elcpmat  22217  pmatcollpw3lem  22285  chfacfisf  22356  chfacfisfcpmat  22357  chfacffsupp  22358  chfacfscmulfsupp  22361  chfacfscmulgsum  22362  chfacfpmmulfsupp  22365  chfacfpmmulgsum  22366  chfacfpmmulgsum2  22367  cayhamlem1  22368  cpmadugsumlemF  22378  cayleyhamilton1  22394  tgcl  22472  pptbas  22511  clsval2  22554  mretopd  22596  lmbr2  22763  cncls2  22777  nrmsep  22861  regsep2  22880  cmpsublem  22903  cmpsub  22904  tgcmp  22905  uncmp  22907  hauscmplem  22910  iunconnlem  22931  1stcrest  22957  2ndcctbss  22959  2ndcsep  22963  dis2ndc  22964  hausllycmp  22998  dislly  23001  kgentopon  23042  1stckgen  23058  kgencn3  23062  ptpjpre1  23075  ptbasin  23081  ptpjopn  23116  dfac14  23122  ptcnplem  23125  txcn  23130  txindis  23138  txdis1cn  23139  ptrescn  23143  txcmplem1  23145  txcmp  23147  txhaus  23151  txlm  23152  tx1stc  23154  txkgen  23156  xkococn  23164  qtopcn  23218  kqreglem1  23245  kqreglem2  23246  kqnrmlem1  23247  kqnrmlem2  23248  hmeoimaf1o  23274  reghmph  23297  nrmhmph  23298  txhmeo  23307  ptuncnv  23311  filconn  23387  fbasrn  23388  fmfnfmlem2  23459  flimfnfcls  23532  cnpfcfi  23544  alexsublem  23548  alexsubALTlem2  23552  alexsubALTlem3  23553  alexsubALTlem4  23554  alexsubALT  23555  ptcmplem3  23558  cnextfval  23566  tsmsxp  23659  imasdsf1olem  23879  bl2in  23906  blssps  23930  blss  23931  blssexps  23932  blssex  23933  blcld  24014  stdbdxmet  24024  met1stc  24030  prdsxmslem2  24038  metcnp3  24049  metcnpi3  24055  txmetcnp  24056  nmo0  24252  nmoid  24259  icccmplem1  24338  icccmp  24341  xrge0tsms  24350  metdseq0  24370  cnheiborlem  24470  cnheibor  24471  cnllycmp  24472  pcoval2  24532  cmetcaulem  24805  iscmet3lem1  24808  iscmet3lem2  24809  equivcau  24817  lmcau  24830  cncmet  24839  ivthlem2  24969  ivthlem3  24970  ovoliunlem2  25020  ovolscalem2  25031  uniioombl  25106  dyaddisj  25113  opnmbllem  25118  volivth  25124  ismbfd  25156  ismbf3d  25171  mbfimaopnlem  25172  mbfinf  25182  itg1addlem4  25216  itg1addlem4OLD  25217  mbfi1fseqlem1  25233  mbfi1fseqlem3  25235  mbfi1fseqlem4  25236  mbfi1fseqlem5  25237  mbfi1fseqlem6  25238  itg2seq  25260  itg2lea  25262  itg2split  25267  itg2cnlem1  25279  bddiblnc  25359  limciun  25411  dvmptfsum  25492  rolle  25507  c1lip1  25514  dvcnvrelem1  25534  dvcnvre  25536  dvcvx  25537  itgsubst  25566  tdeglem4  25577  tdeglem4OLD  25578  mdegmullem  25596  plyco0  25706  coemullem  25764  dgreq0  25779  dgrmul  25784  dgrco  25789  elqaalem2  25833  aannenlem1  25841  aaliou3lem9  25863  ulmres  25900  ulmshftlem  25901  angneg  26308  dcubic  26351  cxploglim  26482  cxploglim2  26483  scvxcvx  26490  lgamgulmlem5  26537  lgamcvg2  26559  ftalem2  26578  basellem3  26587  basellem4  26588  sqff1o  26686  fsumdvdsdiaglem  26687  dvdsflsumcom  26692  dvdsmulf1o  26698  fsumvma2  26717  logfac2  26720  logfacrlim  26727  logexprlim  26728  dchrelbasd  26742  lgsne0  26838  lgsqrlem2  26850  lgsqrmodndvds  26856  gausslemma2dlem1a  26868  lgseisenlem2  26879  lgsquadlem1  26883  lgsquadlem2  26884  lgsquadlem3  26885  lgsquad2lem2  26888  2sqlem8  26929  2sqlem11  26932  2sqreultlem  26950  2sqreunnltlem  26953  chpo1ubb  26984  vmadivsum  26985  rplogsumlem2  26988  rpvmasumlem  26990  dchrmusum2  26997  dchrvmasumlem1  26998  dchrisum0fno1  27014  dchrisum0re  27016  dchrisum0lem1  27019  dchrisum0lem2  27021  dchrisum0lem3  27022  dchrisum0  27023  mulogsumlem  27034  mulog2sumlem2  27038  vmalogdivsum2  27041  logsqvma  27045  log2sumbnd  27047  selberglem3  27050  selberg  27051  selberg2lem  27053  selberg2b  27055  selberg3lem2  27061  pntrmax  27067  pntrsumo1  27068  pntlemn  27103  pntlemp  27113  qabvle  27128  ostthlem1  27130  ostthlem2  27131  ostth2lem2  27137  ostth3  27141  sltres  27165  nosupno  27206  nosupbnd2  27219  noinfno  27221  noinfbnd2  27234  etasslt  27314  cuteq1  27334  addsproplem2  27454  mulsval  27565  precsexlem11  27663  idmot  27788  brbtwn2  28163  colinearalglem4  28167  colinearalg  28168  ax5seglem9  28195  axpaschlem  28198  axcontlem2  28223  axcontlem7  28228  axcontlem8  28229  eengtrkg  28244  upgr1eopALT  28377  uspgredg2vlem  28480  subumgr  28545  nbgr0vtxlem  28612  edgnbusgreu  28624  nb3grprlem1  28637  wlkl1loop  28895  pthdivtx  28986  usgr2pth  29021  crctcshwlkn0  29075  wlklnwwlkln1  29122  wwlksnext  29147  clwwlkccatlem  29242  clwlkclwwlklem2a  29251  clwwlkinwwlk  29293  clwwlkn1loopb  29296  clwwlkf  29300  wwlksext2clwwlk  29310  wwlksubclwwlk  29311  clwwlknscsh  29315  clwwlknon1  29350  clwwlknonex2e  29363  1conngr  29447  n4cyclfrgr  29544  numclwwlk2lem1lem  29595  2clwwlk2clwwlk  29603  numclwwlk1lem2f1  29610  numclwlk1lem1  29622  numclwwlk2lem1  29629  numclwlk2lem2f  29630  numclwwlk7  29644  frgrogt3nreg  29650  grpoidinvlem1  29757  grpoidinvlem3  29759  grporcan  29771  nmlnoubi  30049  blocnilem  30057  ipblnfi  30108  htthlem  30170  ocsh  30536  shmodsi  30642  pjhthlem2  30645  5oalem2  30908  eigposi  31089  nmopub2tALT  31162  nmfnleub2  31179  nmcexi  31279  nmopcoi  31348  kbass3  31371  mdslmd1lem1  31578  mdslmd1lem2  31579  chirredlem2  31644  chirredlem4  31646  mdsymlem3  31658  mdsymlem5  31660  sumdmdii  31668  sumdmdlem  31671  sumdmdlem2  31672  foresf1o  31742  disjxpin  31819  1stpreimas  31927  resf1o  31955  nn0xmulclb  31984  wrdt2ind  32117  xrge0tsmsd  32209  gsumvsca1  32371  gsumvsca2  32372  islinds5  32480  irngnzply1  32755  mdetpmtr1  32803  mdetpmtr2  32804  pstmxmet  32877  qqhghm  32968  qqhrhm  32969  esumpcvgval  33076  volmeas  33229  imambfm  33261  dya2iocnrect  33280  oddpwdc  33353  sseqf  33391  orvcgteel  33466  orvclteel  33471  ballotlemsf1o  33512  bnj1110  33993  bnj1118  33995  f1resveqaeq  34088  txpconn  34223  connpconn  34226  cnllysconn  34236  rellysconn  34242  cvmsss2  34265  cvmlift2lem9  34302  satf00  34365  fmlasuc  34377  mrsubfval  34499  mppsval  34563  dfon2lem6  34760  wzel  34796  ifscgr  35016  cgrxfr  35027  btwnconn1lem5  35063  btwnconn1lem6  35064  btwnconn1lem12  35070  brsegle  35080  finminlem  35203  nn0prpwlem  35207  fnessref  35242  refssfne  35243  neibastop1  35244  topjoin  35250  fnemeet2  35252  bj-prmoore  35996  bj-finsumval0  36166  topdifinffinlem  36228  lindsadd  36481  matunitlindflem2  36485  poimirlem28  36516  poimirlem32  36520  opnmbllem0  36524  mblfinlem1  36525  mblfinlem4  36528  ismblfin  36529  mbfresfi  36534  itg2addnclem  36539  itg2addnclem3  36541  itg2addnc  36542  unirep  36582  frinfm  36603  sdclem2  36610  geomcau  36627  istotbnd3  36639  sstotbnd2  36642  sstotbnd  36643  sstotbnd3  36644  totbndbnd  36657  cntotbnd  36664  ismtyres  36676  heibor1lem  36677  heiborlem1  36679  heiborlem8  36686  ismndo1  36741  isdivrngo  36818  unichnidl  36899  erimeq2  37548  cvlcvr1  38209  ishlat3N  38224  llnmlplnN  38410  islvol2aN  38463  4atlem4c  38472  4atlem4d  38473  isline2  38645  isline3  38647  linepsubclN  38822  lhpexle3lem  38882  lhpjat2  38892  cdlemd4  39072  cdleme0cq  39086  cdleme32fva  39308  cdleme32fvaw  39310  tendo0mul  39697  tendo0mulr  39698  diameetN  39927  dvhvaddcl  39966  dvhvaddcomN  39967  cdlemm10N  39989  dvadiaN  39999  djavalN  40006  dihvalcqat  40110  dihopelvalcpre  40119  djhval  40269  dihjat1lem  40299  sticksstones11  40972  sticksstones22  40984  metakunt15  40999  metakunt16  41000  f1o2d2  41055  evlselvlem  41158  evlselv  41159  fsuppind  41162  mhpind  41166  remul01  41280  zaddcom  41325  zmulcom  41329  prjspertr  41347  prjsprellsp  41353  elrfi  41432  nacsfix  41450  fzsplit1nn0  41492  eldioph2  41500  lzenom  41508  irrapxlem3  41562  pellexlem5  41571  pell1234qrne0  41591  pell1234qrmulcl  41593  pell14qrdich  41607  pell1qrge1  41608  pellqrex  41617  reglogltb  41629  reglogleb  41630  rmxypairf1o  41650  rmxycomplete  41656  monotoddzzfi  41681  congadd  41705  congsym  41707  acongrep  41719  jm2.19lem3  41730  jm2.19lem4  41731  jm2.22  41734  jm2.25  41738  expdiophlem1  41760  wepwsolem  41784  kelac1  41805  lmhmfgsplit  41828  pwslnm  41836  hbtlem6  41871  hbt  41872  mon1psubm  41948  deg1mhm  41949  omord2lim  42050  succlg  42078  onmcl  42081  ofoafo  42106  ofoacom  42111  fzunt  42206  fzuntd  42207  fzunt1d  42208  fzuntgd  42209  iunrelexp0  42453  dssmapnvod  42771  gsumws3  42948  gsumws4  42949  mulltgt0  43706  fnchoice  43713  disjrnmpt2  43886  fzisoeu  44010  fsumiunss  44291  climinf  44322  mullimc  44332  mullimcf  44339  stoweidlem14  44730  stoweidlem17  44733  stoweidlem34  44750  stoweidlem50  44766  fourierdlem42  44865  fourierdlem62  44884  fourierdlem71  44893  fourierdlem76  44898  qndenserrnbllem  45010  subsaliuncl  45074  sge0resplit  45122  upwrdfi  45601  2reu8i  45821  fundcmpsurinjpreimafv  46076  iccpartigtl  46091  prproropf1olem2  46172  prproropf1olem4  46174  paireqne  46179  prmdvdsfmtnof1lem2  46253  bgoldbtbndlem3  46475  bgoldbtbnd  46477  isomushgr  46494  isomuspgrlem2c  46498  uspgrsprf1  46525  subsubmgm  46567  isassintop  46620  subsubrng  46742  2zlidl  46832  2zrngnmrid  46848  rngcinv  46879  rngcinvALTV  46891  ringcinv  46930  funcringcsetcALTV2lem9  46942  ringcinvALTV  46954  funcringcsetclem9ALTV  46965  fldhmsubc  46982  fldhmsubcALTV  47000  mndpsuppss  47047  gsumlsscl  47059  lincsum  47110  lindslinindsimp1  47138  lindslinindimp2lem4  47142  lincresunitlem2  47157  elfzolborelfzop1  47200  elbigo2  47238  digexp  47293  dig1  47294  nn0sumshdiglemB  47306  1arymaptf1  47328  2arymaptf1  47339  itcoval1  47349  itcoval2  47350  itcoval3  47351  itcovalsucov  47354  ackvalsuc1mpt  47364  itschlc0xyqsol  47453  thincciso  47669  indthinc  47672  indthincALT  47673