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  5107  reusv2lem4  5359  axprlem5OLD  5388  fr2nr  5618  somin1  6109  tz7.7  6361  f1oprg  6848  soisores  7305  elovmporab1w  7639  elovmporab1  7640  sorpssi  7708  onint  7769  ordsucelsuc  7800  elxp5  7902  resf1extb  7913  f1oabexg  7921  wemoiso  7955  wemoiso2  7956  el2xptp0  8018  frxp2  8126  frxp3  8133  ressuppss  8165  fprlem1  8282  tz7.48lem  8412  oalimcl  8527  oeeui  8569  nnaordex2  8606  oaabs2  8616  omabs  8618  swoer  8705  ralxpmap  8872  pw2f1olem  9050  enfixsn  9055  mapxpen  9113  mapunen  9116  php  9177  unxpdomlem2  9205  unxpdomlem3  9206  findcard3OLD  9237  isfinite2  9252  fodomfi  9268  domunfican  9279  fodomfiOLD  9288  fissuni  9315  fipreima  9316  indexfi  9318  fsuppsssupp  9339  marypha1lem  9391  marypha2  9397  supmo  9410  infmo  9455  oieu  9499  brwdom2  9533  ixpiunwdom  9550  cantnfval2  9629  cantnfle  9631  cantnflt  9632  cantnf  9653  wemapwe  9657  cnfcom  9660  frrlem15  9717  rankonidlem  9788  r1pwcl  9807  eldju2ndl  9884  eldju2ndr  9885  djuun  9886  infxpenlem  9973  infxpenc2lem1  9979  fseqenlem1  9984  dfac8clem  9992  mappwen  10072  dfac3  10081  dfac5  10089  dfac12lem3  10106  infunsdom  10173  coftr  10233  ssfin4  10270  domfin4  10271  fin23lem26  10285  fin23lem22  10287  fin23lem28  10300  fin23lem32  10304  fin23lem40  10311  isf32lem5  10317  compssiso  10334  isf34lem4  10337  isfin1-3  10346  fin1a2lem13  10372  hsmexlem2  10387  hsmexlem4  10389  zorn2lem1  10456  ttukeylem6  10474  iundom2g  10500  konigthlem  10528  pwcfsdom  10543  fpwwe2lem11  10601  fpwwe2  10603  pwfseqlem3  10620  winalim2  10656  r1wunlim  10697  inttsk  10734  inar1  10735  grur1  10780  nqereq  10895  ltexprlem7  11002  prlem936  11007  00id  11356  addlid  11364  ltord1  11711  divdiv1  11900  divdiv2  11901  conjmul  11906  ltdivmul  12065  ledivmul  12066  lt2mul2div  12068  ltdiv23  12081  lediv23  12082  lediv12a  12083  ledivp1  12092  negfi  12139  nn0nndivcl  12521  nn0ge0div  12610  peano2uz2  12629  peano5uzi  12630  eluzp1m1  12826  qbtwnre  13166  xralrple  13172  xleadd1a  13220  xmulge0  13251  xmulass  13254  xlemul1a  13255  iooshf  13394  divelunit  13462  eluzgtdifelfzo  13695  modadd1  13877  modmul1  13896  seqcl2  13992  seqfveq2  13996  seqid2  14020  seqhomo  14021  seqdistr  14025  mulexpz  14074  leexp2r  14146  expnlbnd2  14206  expmulnbnd  14207  hashmap  14407  hashfun  14409  hashbclem  14424  hashfacen  14426  hashf1lem2  14428  hashf1  14429  ccatsymb  14554  swrdwrdsymb  14634  swrdsb0eq  14635  ccatpfx  14673  swrdswrd  14677  wrdind  14694  wrd2ind  14695  swrdccatin1  14697  swrdccatin2  14701  pfxccatin12lem2  14703  pfxccatin12  14705  swrdccat  14707  repswswrd  14756  0csh0  14765  cshwidxmod  14775  2cshw  14785  cshweqrep  14793  relexp0g  14995  relexpsucnnr  14998  relexpindlem  15036  01sqrexlem1  15215  01sqrexlem6  15220  rlim  15468  rlimclim1  15518  climsup  15643  caurcvg2  15651  caucvgb  15653  iseralt  15658  sumss  15697  fsum2dlem  15743  mptfzshft  15751  modfsummod  15767  o1fsum  15786  incexclem  15809  divrcnv  15825  flo1  15827  fprodrev  15950  fprod2dlem  15953  ruclem6  16210  moddvds  16240  dvdsaddre2b  16284  dvdsflip  16294  addmodlteqALT  16302  nn0o  16360  fldivndvdslt  16393  bitsf1ocnv  16421  bitsf1  16423  sadcaddlem  16434  bezoutlem2  16517  bezoutlem4  16519  lcmgcdlem  16583  prmind2  16662  isprm5  16684  isprm6  16691  prmdvdsncoprmbd  16704  cncongrprm  16706  hashdvds  16752  crth  16755  eulerthlem2  16759  prmdiveq  16763  hashgcdlem  16765  hashgcdeq  16767  iserodd  16813  pclem  16816  pcprendvds2  16819  pcexp  16837  pcneg  16852  pc2dvds  16857  pcmpt  16870  prmpwdvds  16882  pockthg  16884  prmreclem5  16898  4sqlem11  16933  ramub2  16992  ramubcl  16996  ram0  17000  ramub1lem2  17005  ramcl  17007  prmgaplem3  17031  prmgaplem6  17034  setscom  17157  sscpwex  17784  initoeu2  17985  setcinv  18059  funcestrcsetclem9  18116  funcsetcestrclem9  18131  fullsetcestrc  18134  1stfcl  18165  2ndfcl  18166  hofpropd  18235  isacs3lem  18508  isacs4lem  18510  acsmap2d  18521  subsubmgm  18644  submnd0  18697  mndpsuppss  18699  subsubm  18750  insubm  18752  frmdup1  18798  frmdup3lem  18800  sgrp2nmndlem2  18858  isgrpinv  18932  subsubg  19088  cycsubgcl  19145  conjghm  19188  qusghm  19194  gsumwrev  19305  gsmsymgrfixlem1  19364  symgfixelsi  19372  symgsssg  19404  symgfisg  19405  psgnunilem2  19432  odf1o2  19510  sylow1lem1  19535  odcau  19541  pgpfi  19542  pgpssslw  19551  fislw  19562  efgtlen  19663  efginvrel2  19664  efgrelexlemb  19687  efgredeu  19689  efgcpbllemb  19692  frgpup1  19712  lt6abl  19832  gsum2d  19909  gsum2d2lem  19910  gsum2d2  19911  telgsumfzslem  19925  dmdprdsplit2lem  19984  ablfacrp  20005  pgpfac1lem3  20016  gsummgp0  20234  irredrmul  20343  subsubrng  20479  subsubrg  20514  rngcinv  20553  ringcinv  20587  fldhmsubc  20701  islss4  20875  lspextmo  20970  lspsnat  21062  prmirredlem  21389  znf1o  21468  znidomb  21478  frgpcyg  21490  psgnghm  21496  psgndiflemB  21516  frlmlbs  21713  frlmup1  21714  lindfind  21732  islindf3  21742  lindfmm  21743  issubassa3  21782  resspsradd  21891  resspsrmul  21892  psdmul  22060  coe1tmmul2  22169  pf1ind  22249  mamulid  22335  mat1dimelbas  22365  mdetdiaglem  22492  mdetralt2  22503  mndifsplit  22530  smadiadetglem2  22566  1elcpmat  22609  pmatcollpw3lem  22677  chfacfisf  22748  chfacfisfcpmat  22749  chfacffsupp  22750  chfacfscmulfsupp  22753  chfacfscmulgsum  22754  chfacfpmmulfsupp  22757  chfacfpmmulgsum  22758  chfacfpmmulgsum2  22759  cayhamlem1  22760  cpmadugsumlemF  22770  cayleyhamilton1  22786  tgcl  22863  pptbas  22902  clsval2  22944  mretopd  22986  lmbr2  23153  cncls2  23167  nrmsep  23251  regsep2  23270  cmpsublem  23293  cmpsub  23294  tgcmp  23295  uncmp  23297  hauscmplem  23300  iunconnlem  23321  1stcrest  23347  2ndcctbss  23349  2ndcsep  23353  dis2ndc  23354  hausllycmp  23388  dislly  23391  kgentopon  23432  1stckgen  23448  kgencn3  23452  ptpjpre1  23465  ptbasin  23471  ptpjopn  23506  dfac14  23512  ptcnplem  23515  txcn  23520  txindis  23528  txdis1cn  23529  ptrescn  23533  txcmplem1  23535  txcmp  23537  txhaus  23541  txlm  23542  tx1stc  23544  txkgen  23546  xkococn  23554  qtopcn  23608  kqreglem1  23635  kqreglem2  23636  kqnrmlem1  23637  kqnrmlem2  23638  hmeoimaf1o  23664  reghmph  23687  nrmhmph  23688  txhmeo  23697  ptuncnv  23701  filconn  23777  fbasrn  23778  fmfnfmlem2  23849  flimfnfcls  23922  cnpfcfi  23934  alexsublem  23938  alexsubALTlem2  23942  alexsubALTlem3  23943  alexsubALTlem4  23944  alexsubALT  23945  ptcmplem3  23948  cnextfval  23956  tsmsxp  24049  imasdsf1olem  24268  bl2in  24295  blssps  24319  blss  24320  blssexps  24321  blssex  24322  blcld  24400  stdbdxmet  24410  met1stc  24416  prdsxmslem2  24424  metcnp3  24435  metcnpi3  24441  txmetcnp  24442  nmo0  24630  nmoid  24637  icccmplem1  24718  icccmp  24721  xrge0tsms  24730  metdseq0  24750  cnheiborlem  24860  cnheibor  24861  cnllycmp  24862  pcoval2  24923  cmetcaulem  25195  iscmet3lem1  25198  iscmet3lem2  25199  equivcau  25207  lmcau  25220  cncmet  25229  ivthlem2  25360  ivthlem3  25361  ovoliunlem2  25411  ovolscalem2  25422  uniioombl  25497  dyaddisj  25504  opnmbllem  25509  volivth  25515  ismbfd  25547  ismbf3d  25562  mbfimaopnlem  25563  mbfinf  25573  itg1addlem4  25607  mbfi1fseqlem1  25623  mbfi1fseqlem3  25625  mbfi1fseqlem4  25626  mbfi1fseqlem5  25627  mbfi1fseqlem6  25628  itg2seq  25650  itg2lea  25652  itg2split  25657  itg2cnlem1  25669  bddiblnc  25750  limciun  25802  dvmptfsum  25886  rolle  25901  c1lip1  25909  dvcnvrelem1  25929  dvcnvre  25931  dvcvx  25932  itgsubst  25963  tdeglem4  25972  mdegmullem  25990  plyco0  26104  coemullem  26162  dgreq0  26178  dgrmul  26183  dgrco  26188  elqaalem2  26235  aannenlem1  26243  aaliou3lem9  26265  ulmres  26304  ulmshftlem  26305  angneg  26720  dcubic  26763  cxploglim  26895  cxploglim2  26896  scvxcvx  26903  lgamgulmlem5  26950  lgamcvg2  26972  ftalem2  26991  basellem3  27000  basellem4  27001  sqff1o  27099  fsumdvdsdiaglem  27100  dvdsflsumcom  27105  mpodvdsmulf1o  27111  dvdsmulf1o  27113  fsumvma2  27132  logfac2  27135  logfacrlim  27142  logexprlim  27143  dchrelbasd  27157  lgsne0  27253  lgsqrlem2  27265  lgsqrmodndvds  27271  gausslemma2dlem1a  27283  lgseisenlem2  27294  lgsquadlem1  27298  lgsquadlem2  27299  lgsquadlem3  27300  lgsquad2lem2  27303  2sqlem8  27344  2sqlem11  27347  2sqreultlem  27365  2sqreunnltlem  27368  chpo1ubb  27399  vmadivsum  27400  rplogsumlem2  27403  rpvmasumlem  27405  dchrmusum2  27412  dchrvmasumlem1  27413  dchrisum0fno1  27429  dchrisum0re  27431  dchrisum0lem1  27434  dchrisum0lem2  27436  dchrisum0lem3  27437  dchrisum0  27438  mulogsumlem  27449  mulog2sumlem2  27453  vmalogdivsum2  27456  logsqvma  27460  log2sumbnd  27462  selberglem3  27465  selberg  27466  selberg2lem  27468  selberg2b  27470  selberg3lem2  27476  pntrmax  27482  pntrsumo1  27483  pntlemn  27518  pntlemp  27528  qabvle  27543  ostthlem1  27545  ostthlem2  27546  ostth2lem2  27552  ostth3  27556  sltres  27581  nosupno  27622  nosupbnd2  27635  noinfno  27637  noinfbnd2  27650  etasslt  27732  cuteq1  27753  addsproplem2  27884  mulsval  28019  precsexlem11  28126  n0sfincut  28253  zmulscld  28292  idmot  28471  brbtwn2  28839  colinearalglem4  28843  colinearalg  28844  ax5seglem9  28871  axpaschlem  28874  axcontlem2  28899  axcontlem7  28904  axcontlem8  28905  eengtrkg  28920  upgr1eopALT  29051  uspgredg2vlem  29157  subumgr  29222  nbgr0edglem  29290  edgnbusgreu  29301  nb3grprlem1  29314  wlkl1loop  29573  pthdivtx  29664  usgr2pth  29701  crctcshwlkn0  29758  wlklnwwlkln1  29805  wwlksnext  29830  clwwlkccatlem  29925  clwlkclwwlklem2a  29934  clwwlkinwwlk  29976  clwwlkn1loopb  29979  clwwlkf  29983  wwlksext2clwwlk  29993  wwlksubclwwlk  29994  clwwlknscsh  29998  clwwlknon1  30033  clwwlknonex2e  30046  1conngr  30130  n4cyclfrgr  30227  numclwwlk2lem1lem  30278  2clwwlk2clwwlk  30286  numclwwlk1lem2f1  30293  numclwlk1lem1  30305  numclwwlk2lem1  30312  numclwlk2lem2f  30313  numclwwlk7  30327  frgrogt3nreg  30333  grpoidinvlem1  30440  grpoidinvlem3  30442  grporcan  30454  nmlnoubi  30732  blocnilem  30740  ipblnfi  30791  htthlem  30853  ocsh  31219  shmodsi  31325  pjhthlem2  31328  5oalem2  31591  eigposi  31772  nmopub2tALT  31845  nmfnleub2  31862  nmcexi  31962  nmopcoi  32031  kbass3  32054  mdslmd1lem1  32261  mdslmd1lem2  32262  chirredlem2  32327  chirredlem4  32329  mdsymlem3  32341  mdsymlem5  32343  sumdmdii  32351  sumdmdlem  32354  sumdmdlem2  32355  foresf1o  32440  disjxpin  32524  1stpreimas  32636  resf1o  32660  nn0xmulclb  32701  wrdt2ind  32882  xrge0tsmsd  33009  gsumvsca1  33186  gsumvsca2  33187  islinds5  33345  1arithidomlem2  33514  irngnzply1  33693  mdetpmtr1  33820  mdetpmtr2  33821  pstmxmet  33894  qqhghm  33985  qqhrhm  33986  esumpcvgval  34075  volmeas  34228  imambfm  34260  dya2iocnrect  34279  oddpwdc  34352  sseqf  34390  orvcgteel  34466  orvclteel  34471  ballotlemsf1o  34512  bnj1110  34979  bnj1118  34981  f1resveqaeq  35082  txpconn  35226  connpconn  35229  cnllysconn  35239  rellysconn  35245  cvmsss2  35268  cvmlift2lem9  35305  satf00  35368  fmlasuc  35380  mrsubfval  35502  mppsval  35566  dfon2lem6  35783  wzel  35819  ifscgr  36039  cgrxfr  36050  btwnconn1lem5  36086  btwnconn1lem6  36087  btwnconn1lem12  36093  brsegle  36103  finminlem  36313  nn0prpwlem  36317  fnessref  36352  refssfne  36353  neibastop1  36354  topjoin  36360  fnemeet2  36362  weiunse  36463  bj-prmoore  37110  bj-finsumval0  37280  topdifinffinlem  37342  lindsadd  37614  matunitlindflem2  37618  poimirlem28  37649  poimirlem32  37653  opnmbllem0  37657  mblfinlem1  37658  mblfinlem4  37661  ismblfin  37662  mbfresfi  37667  itg2addnclem  37672  itg2addnclem3  37674  itg2addnc  37675  unirep  37715  frinfm  37736  sdclem2  37743  geomcau  37760  istotbnd3  37772  sstotbnd2  37775  sstotbnd  37776  sstotbnd3  37777  totbndbnd  37790  cntotbnd  37797  ismtyres  37809  heibor1lem  37810  heiborlem1  37812  heiborlem8  37819  ismndo1  37874  isdivrngo  37951  unichnidl  38032  erimeq2  38677  cvlcvr1  39339  ishlat3N  39354  llnmlplnN  39540  islvol2aN  39593  4atlem4c  39602  4atlem4d  39603  isline2  39775  isline3  39777  linepsubclN  39952  lhpexle3lem  40012  lhpjat2  40022  cdlemd4  40202  cdleme0cq  40216  cdleme32fva  40438  cdleme32fvaw  40440  tendo0mul  40827  tendo0mulr  40828  diameetN  41057  dvhvaddcl  41096  dvhvaddcomN  41097  cdlemm10N  41119  dvadiaN  41129  djavalN  41136  dihvalcqat  41240  dihopelvalcpre  41249  djhval  41399  dihjat1lem  41429  sticksstones11  42151  sticksstones22  42163  f1o2d2  42228  remul01  42402  zaddcom  42459  zmulcom  42463  fidomncyc  42530  evlselvlem  42581  evlselv  42582  fsuppind  42585  mhpind  42589  prjspertr  42600  prjsprellsp  42606  elrfi  42689  nacsfix  42707  fzsplit1nn0  42749  eldioph2  42757  lzenom  42765  irrapxlem3  42819  pellexlem5  42828  pell1234qrne0  42848  pell1234qrmulcl  42850  pell14qrdich  42864  pell1qrge1  42865  pellqrex  42874  reglogltb  42886  reglogleb  42887  rmxypairf1o  42907  rmxycomplete  42913  monotoddzzfi  42938  congadd  42962  congsym  42964  acongrep  42976  jm2.19lem3  42987  jm2.19lem4  42988  jm2.22  42991  jm2.25  42995  expdiophlem1  43017  wepwsolem  43038  kelac1  43059  lmhmfgsplit  43082  pwslnm  43090  hbtlem6  43125  hbt  43126  mon1psubm  43195  deg1mhm  43196  omord2lim  43296  succlg  43324  onmcl  43327  ofoafo  43352  ofoacom  43357  fzunt  43451  fzuntd  43452  fzunt1d  43453  fzuntgd  43454  iunrelexp0  43698  dssmapnvod  44016  gsumws3  44192  gsumws4  44193  mulltgt0  45023  fnchoice  45030  disjrnmpt2  45189  fzisoeu  45305  fsumiunss  45580  climinf  45611  mullimc  45621  mullimcf  45628  stoweidlem14  46019  stoweidlem17  46022  stoweidlem34  46039  stoweidlem50  46055  fourierdlem42  46154  fourierdlem62  46173  fourierdlem71  46182  fourierdlem76  46187  qndenserrnbllem  46299  subsaliuncl  46363  sge0resplit  46411  upwrdfi  46892  3f1oss1  47080  2reu8i  47118  addmodne  47349  fundcmpsurinjpreimafv  47413  iccpartigtl  47428  prproropf1olem2  47509  prproropf1olem4  47511  paireqne  47516  prmdvdsfmtnof1lem2  47590  bgoldbtbndlem3  47812  bgoldbtbnd  47814  grimcnv  47892  gricushgr  47921  cycldlenngric  47932  grimedg  47939  grtrimap  47951  isubgr3stgrlem6  47974  isubgr3stgrlem7  47975  isubgr3stgrlem8  47976  isubgr3stgrlem9  47977  grlimfn  47982  gpgedg2iv  48062  gpg5nbgrvtx03starlem2  48064  gpg5nbgrvtx13starlem2  48067  uspgrsprf1  48139  isassintop  48202  2zlidl  48232  2zrngnmrid  48248  rngcinvALTV  48268  funcringcsetcALTV2lem9  48290  ringcinvALTV  48302  funcringcsetclem9ALTV  48313  fldhmsubcALTV  48325  gsumlsscl  48372  lincsum  48422  lindslinindsimp1  48450  lindslinindimp2lem4  48454  lincresunitlem2  48469  elfzolborelfzop1  48512  elbigo2  48545  digexp  48600  dig1  48601  nn0sumshdiglemB  48613  1arymaptf1  48635  2arymaptf1  48646  itcoval1  48656  itcoval2  48657  itcoval3  48658  itcovalsucov  48661  ackvalsuc1mpt  48671  itschlc0xyqsol  48760  brab2dd  48820  dmrnxp  48829  xpco2  48849  initopropd  49236  termopropd  49237  zeroopropd  49238  prcofpropd  49372  thincciso  49446  indthinc  49455  indthincALT  49456  oduoppcciso  49559  lanpropd  49608  ranpropd  49609