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  5093  reusv2lem4  5344  axprlem5OLD  5373  fr2nr  5599  somin1  6088  tz7.7  6341  f1oprg  6818  soisores  7271  elovmporab1w  7603  elovmporab1  7604  sorpssi  7672  onint  7733  ordsucelsuc  7762  elxp5  7863  resf1extb  7874  f1oabexg  7882  wemoiso  7915  wemoiso2  7916  el2xptp0  7978  frxp2  8084  frxp3  8091  ressuppss  8123  fprlem1  8240  tz7.48lem  8370  oalimcl  8485  oeeui  8528  nnaordex2  8565  oaabs2  8575  omabs  8577  swoer  8664  ralxpmap  8832  pw2f1olem  9007  enfixsn  9012  mapxpen  9069  mapunen  9072  php  9129  unxpdomlem2  9155  unxpdomlem3  9156  isfinite2  9196  fodomfi  9210  domunfican  9220  fodomfiOLD  9228  fissuni  9255  fipreima  9256  indexfi  9258  fsuppsssupp  9282  marypha1lem  9334  marypha2  9340  supmo  9353  infmo  9398  oieu  9442  brwdom2  9476  ixpiunwdom  9493  cantnfval2  9576  cantnfle  9578  cantnflt  9579  cantnf  9600  wemapwe  9604  cnfcom  9607  frrlem15  9667  rankonidlem  9738  r1pwcl  9757  eldju2ndl  9834  eldju2ndr  9835  djuun  9836  infxpenlem  9921  infxpenc2lem1  9927  fseqenlem1  9932  dfac8clem  9940  mappwen  10020  dfac3  10029  dfac5  10037  dfac12lem3  10054  infunsdom  10121  coftr  10181  ssfin4  10218  domfin4  10219  fin23lem26  10233  fin23lem22  10235  fin23lem28  10248  fin23lem32  10252  fin23lem40  10259  isf32lem5  10265  compssiso  10282  isf34lem4  10285  isfin1-3  10294  fin1a2lem13  10320  hsmexlem2  10335  hsmexlem4  10337  zorn2lem1  10404  ttukeylem6  10422  iundom2g  10448  konigthlem  10477  pwcfsdom  10492  fpwwe2lem11  10550  fpwwe2  10552  pwfseqlem3  10569  winalim2  10605  r1wunlim  10646  inttsk  10683  inar1  10684  grur1  10729  nqereq  10844  ltexprlem7  10951  prlem936  10956  00id  11306  addlid  11314  ltord1  11661  divdiv1  11850  divdiv2  11851  conjmul  11856  ltdivmul  12015  ledivmul  12016  lt2mul2div  12018  ltdiv23  12031  lediv23  12032  lediv12a  12033  ledivp1  12042  negfi  12089  nn0nndivcl  12471  nn0ge0div  12559  peano2uz2  12578  peano5uzi  12579  eluzp1m1  12775  qbtwnre  13112  xralrple  13118  xleadd1a  13166  xmulge0  13197  xmulass  13200  xlemul1a  13201  iooshf  13340  divelunit  13408  eluzgtdifelfzo  13641  modadd1  13826  modmul1  13845  seqcl2  13941  seqfveq2  13945  seqid2  13969  seqhomo  13970  seqdistr  13974  mulexpz  14023  leexp2r  14095  expnlbnd2  14155  expmulnbnd  14156  hashmap  14356  hashfun  14358  hashbclem  14373  hashfacen  14375  hashf1lem2  14377  hashf1  14378  ccatsymb  14504  swrdwrdsymb  14584  swrdsb0eq  14585  ccatpfx  14622  swrdswrd  14626  wrdind  14643  wrd2ind  14644  swrdccatin1  14646  swrdccatin2  14650  pfxccatin12lem2  14652  pfxccatin12  14654  swrdccat  14656  repswswrd  14705  0csh0  14714  cshwidxmod  14724  2cshw  14734  cshweqrep  14742  relexp0g  14943  relexpsucnnr  14946  relexpindlem  14984  01sqrexlem1  15163  01sqrexlem6  15168  rlim  15416  rlimclim1  15466  climsup  15591  caurcvg2  15599  caucvgb  15601  iseralt  15606  sumss  15645  fsum2dlem  15691  mptfzshft  15699  modfsummod  15715  o1fsum  15734  incexclem  15757  divrcnv  15773  flo1  15775  fprodrev  15898  fprod2dlem  15901  ruclem6  16158  moddvds  16188  dvdsaddre2b  16232  dvdsflip  16242  addmodlteqALT  16250  nn0o  16308  fldivndvdslt  16341  bitsf1ocnv  16369  bitsf1  16371  sadcaddlem  16382  bezoutlem2  16465  bezoutlem4  16467  lcmgcdlem  16531  prmind2  16610  isprm5  16632  isprm6  16639  prmdvdsncoprmbd  16652  cncongrprm  16654  hashdvds  16700  crth  16703  eulerthlem2  16707  prmdiveq  16711  hashgcdlem  16713  hashgcdeq  16715  iserodd  16761  pclem  16764  pcprendvds2  16767  pcexp  16785  pcneg  16800  pc2dvds  16805  pcmpt  16818  prmpwdvds  16830  pockthg  16832  prmreclem5  16846  4sqlem11  16881  ramub2  16940  ramubcl  16944  ram0  16948  ramub1lem2  16953  ramcl  16955  prmgaplem3  16979  prmgaplem6  16982  setscom  17105  sscpwex  17737  initoeu2  17938  setcinv  18012  funcestrcsetclem9  18069  funcsetcestrclem9  18084  fullsetcestrc  18087  1stfcl  18118  2ndfcl  18119  hofpropd  18188  isacs3lem  18463  isacs4lem  18465  acsmap2d  18476  chnflenfi  18549  subsubmgm  18633  submnd0  18686  mndpsuppss  18688  subsubm  18739  insubm  18741  frmdup1  18787  frmdup3lem  18789  sgrp2nmndlem2  18847  isgrpinv  18921  subsubg  19077  cycsubgcl  19133  conjghm  19176  qusghm  19182  gsumwrev  19293  gsmsymgrfixlem1  19354  symgfixelsi  19362  symgsssg  19394  symgfisg  19395  psgnunilem2  19422  odf1o2  19500  sylow1lem1  19525  odcau  19531  pgpfi  19532  pgpssslw  19541  fislw  19552  efgtlen  19653  efginvrel2  19654  efgrelexlemb  19677  efgredeu  19679  efgcpbllemb  19682  frgpup1  19702  lt6abl  19822  gsum2d  19899  gsum2d2lem  19900  gsum2d2  19901  telgsumfzslem  19915  dmdprdsplit2lem  19974  ablfacrp  19995  pgpfac1lem3  20006  gsummgp0  20251  irredrmul  20361  subsubrng  20494  subsubrg  20529  rngcinv  20568  ringcinv  20602  fldhmsubc  20716  islss4  20911  lspextmo  21006  lspsnat  21098  prmirredlem  21425  znf1o  21504  znidomb  21514  frgpcyg  21526  psgnghm  21533  psgndiflemB  21553  frlmlbs  21750  frlmup1  21751  lindfind  21769  islindf3  21779  lindfmm  21780  issubassa3  21819  resspsradd  21928  resspsrmul  21929  psdmul  22107  coe1tmmul2  22216  pf1ind  22297  mamulid  22383  mat1dimelbas  22413  mdetdiaglem  22540  mdetralt2  22551  mndifsplit  22578  smadiadetglem2  22614  1elcpmat  22657  pmatcollpw3lem  22725  chfacfisf  22796  chfacfisfcpmat  22797  chfacffsupp  22798  chfacfscmulfsupp  22801  chfacfscmulgsum  22802  chfacfpmmulfsupp  22805  chfacfpmmulgsum  22806  chfacfpmmulgsum2  22807  cayhamlem1  22808  cpmadugsumlemF  22818  cayleyhamilton1  22834  tgcl  22911  pptbas  22950  clsval2  22992  mretopd  23034  lmbr2  23201  cncls2  23215  nrmsep  23299  regsep2  23318  cmpsublem  23341  cmpsub  23342  tgcmp  23343  uncmp  23345  hauscmplem  23348  iunconnlem  23369  1stcrest  23395  2ndcctbss  23397  2ndcsep  23401  dis2ndc  23402  hausllycmp  23436  dislly  23439  kgentopon  23480  1stckgen  23496  kgencn3  23500  ptpjpre1  23513  ptbasin  23519  ptpjopn  23554  dfac14  23560  ptcnplem  23563  txcn  23568  txindis  23576  txdis1cn  23577  ptrescn  23581  txcmplem1  23583  txcmp  23585  txhaus  23589  txlm  23590  tx1stc  23592  txkgen  23594  xkococn  23602  qtopcn  23656  kqreglem1  23683  kqreglem2  23684  kqnrmlem1  23685  kqnrmlem2  23686  hmeoimaf1o  23712  reghmph  23735  nrmhmph  23736  txhmeo  23745  ptuncnv  23749  filconn  23825  fbasrn  23826  fmfnfmlem2  23897  flimfnfcls  23970  cnpfcfi  23982  alexsublem  23986  alexsubALTlem2  23990  alexsubALTlem3  23991  alexsubALTlem4  23992  alexsubALT  23993  ptcmplem3  23996  cnextfval  24004  tsmsxp  24097  imasdsf1olem  24315  bl2in  24342  blssps  24366  blss  24367  blssexps  24368  blssex  24369  blcld  24447  stdbdxmet  24457  met1stc  24463  prdsxmslem2  24471  metcnp3  24482  metcnpi3  24488  txmetcnp  24489  nmo0  24677  nmoid  24684  icccmplem1  24765  icccmp  24768  xrge0tsms  24777  metdseq0  24797  cnheiborlem  24907  cnheibor  24908  cnllycmp  24909  pcoval2  24970  cmetcaulem  25242  iscmet3lem1  25245  iscmet3lem2  25246  equivcau  25254  lmcau  25267  cncmet  25276  ivthlem2  25407  ivthlem3  25408  ovoliunlem2  25458  ovolscalem2  25469  uniioombl  25544  dyaddisj  25551  opnmbllem  25556  volivth  25562  ismbfd  25594  ismbf3d  25609  mbfimaopnlem  25610  mbfinf  25620  itg1addlem4  25654  mbfi1fseqlem1  25670  mbfi1fseqlem3  25672  mbfi1fseqlem4  25673  mbfi1fseqlem5  25674  mbfi1fseqlem6  25675  itg2seq  25697  itg2lea  25699  itg2split  25704  itg2cnlem1  25716  bddiblnc  25797  limciun  25849  dvmptfsum  25933  rolle  25948  c1lip1  25956  dvcnvrelem1  25976  dvcnvre  25978  dvcvx  25979  itgsubst  26010  tdeglem4  26019  mdegmullem  26037  plyco0  26151  coemullem  26209  dgreq0  26225  dgrmul  26230  dgrco  26235  elqaalem2  26282  aannenlem1  26290  aaliou3lem9  26312  ulmres  26351  ulmshftlem  26352  angneg  26767  dcubic  26810  cxploglim  26942  cxploglim2  26943  scvxcvx  26950  lgamgulmlem5  26997  lgamcvg2  27019  ftalem2  27038  basellem3  27047  basellem4  27048  sqff1o  27146  fsumdvdsdiaglem  27147  dvdsflsumcom  27152  mpodvdsmulf1o  27158  dvdsmulf1o  27160  fsumvma2  27179  logfac2  27182  logfacrlim  27189  logexprlim  27190  dchrelbasd  27204  lgsne0  27300  lgsqrlem2  27312  lgsqrmodndvds  27318  gausslemma2dlem1a  27330  lgseisenlem2  27341  lgsquadlem1  27345  lgsquadlem2  27346  lgsquadlem3  27347  lgsquad2lem2  27350  2sqlem8  27391  2sqlem11  27394  2sqreultlem  27412  2sqreunnltlem  27415  chpo1ubb  27446  vmadivsum  27447  rplogsumlem2  27450  rpvmasumlem  27452  dchrmusum2  27459  dchrvmasumlem1  27460  dchrisum0fno1  27476  dchrisum0re  27478  dchrisum0lem1  27481  dchrisum0lem2  27483  dchrisum0lem3  27484  dchrisum0  27485  mulogsumlem  27496  mulog2sumlem2  27500  vmalogdivsum2  27503  logsqvma  27507  log2sumbnd  27509  selberglem3  27512  selberg  27513  selberg2lem  27515  selberg2b  27517  selberg3lem2  27523  pntrmax  27529  pntrsumo1  27530  pntlemn  27565  pntlemp  27575  qabvle  27590  ostthlem1  27592  ostthlem2  27593  ostth2lem2  27599  ostth3  27603  sltres  27628  nosupno  27669  nosupbnd2  27682  noinfno  27684  noinfbnd2  27697  etasslt  27781  cuteq1  27805  addsproplem2  27940  mulsval  28078  precsexlem11  28185  n0sfincut  28315  zmulscld  28355  idmot  28558  brbtwn2  28927  colinearalglem4  28931  colinearalg  28932  ax5seglem9  28959  axpaschlem  28962  axcontlem2  28987  axcontlem7  28992  axcontlem8  28993  eengtrkg  29008  upgr1eopALT  29139  uspgredg2vlem  29245  subumgr  29310  nbgr0edglem  29378  edgnbusgreu  29389  nb3grprlem1  29402  wlkl1loop  29660  pthdivtx  29749  usgr2pth  29786  crctcshwlkn0  29843  wlklnwwlkln1  29890  wwlksnext  29915  clwwlkccatlem  30013  clwlkclwwlklem2a  30022  clwwlkinwwlk  30064  clwwlkn1loopb  30067  clwwlkf  30071  wwlksext2clwwlk  30081  wwlksubclwwlk  30082  clwwlknscsh  30086  clwwlknon1  30121  clwwlknonex2e  30134  1conngr  30218  n4cyclfrgr  30315  numclwwlk2lem1lem  30366  2clwwlk2clwwlk  30374  numclwwlk1lem2f1  30381  numclwlk1lem1  30393  numclwwlk2lem1  30400  numclwlk2lem2f  30401  numclwwlk7  30415  frgrogt3nreg  30421  grpoidinvlem1  30528  grpoidinvlem3  30530  grporcan  30542  nmlnoubi  30820  blocnilem  30828  ipblnfi  30879  htthlem  30941  ocsh  31307  shmodsi  31413  pjhthlem2  31416  5oalem2  31679  eigposi  31860  nmopub2tALT  31933  nmfnleub2  31950  nmcexi  32050  nmopcoi  32119  kbass3  32142  mdslmd1lem1  32349  mdslmd1lem2  32350  chirredlem2  32415  chirredlem4  32417  mdsymlem3  32429  mdsymlem5  32431  sumdmdii  32439  sumdmdlem  32442  sumdmdlem2  32443  foresf1o  32528  disjxpin  32612  1stpreimas  32734  resf1o  32758  nn0xmulclb  32800  wrdt2ind  32984  xrge0tsmsd  33104  gsumvsca1  33257  gsumvsca2  33258  islinds5  33397  1arithidomlem2  33566  mplvrpmmhm  33660  irngnzply1  33797  mdetpmtr1  33929  mdetpmtr2  33930  pstmxmet  34003  qqhghm  34094  qqhrhm  34095  esumpcvgval  34184  volmeas  34337  imambfm  34368  dya2iocnrect  34387  oddpwdc  34460  sseqf  34498  orvcgteel  34574  orvclteel  34579  ballotlemsf1o  34620  bnj1110  35087  bnj1118  35089  f1resveqaeq  35190  txpconn  35375  connpconn  35378  cnllysconn  35388  rellysconn  35394  cvmsss2  35417  cvmlift2lem9  35454  satf00  35517  fmlasuc  35529  mrsubfval  35651  mppsval  35715  dfon2lem6  35929  wzel  35965  ifscgr  36187  cgrxfr  36198  btwnconn1lem5  36234  btwnconn1lem6  36235  btwnconn1lem12  36241  brsegle  36251  finminlem  36461  nn0prpwlem  36465  fnessref  36500  refssfne  36501  neibastop1  36502  topjoin  36508  fnemeet2  36510  weiunse  36611  bj-prmoore  37259  bj-finsumval0  37429  topdifinffinlem  37491  lindsadd  37753  matunitlindflem2  37757  poimirlem28  37788  poimirlem32  37792  opnmbllem0  37796  mblfinlem1  37797  mblfinlem4  37800  ismblfin  37801  mbfresfi  37806  itg2addnclem  37811  itg2addnclem3  37813  itg2addnc  37814  unirep  37854  frinfm  37875  sdclem2  37882  geomcau  37899  istotbnd3  37911  sstotbnd2  37914  sstotbnd  37915  sstotbnd3  37916  totbndbnd  37929  cntotbnd  37936  ismtyres  37948  heibor1lem  37949  heiborlem1  37951  heiborlem8  37958  ismndo1  38013  isdivrngo  38090  unichnidl  38171  erimeq2  38876  cvlcvr1  39538  ishlat3N  39553  llnmlplnN  39738  islvol2aN  39791  4atlem4c  39800  4atlem4d  39801  isline2  39973  isline3  39975  linepsubclN  40150  lhpexle3lem  40210  lhpjat2  40220  cdlemd4  40400  cdleme0cq  40414  cdleme32fva  40636  cdleme32fvaw  40638  tendo0mul  41025  tendo0mulr  41026  diameetN  41255  dvhvaddcl  41294  dvhvaddcomN  41295  cdlemm10N  41317  dvadiaN  41327  djavalN  41334  dihvalcqat  41438  dihopelvalcpre  41447  djhval  41597  dihjat1lem  41627  sticksstones11  42349  sticksstones22  42361  f1o2d2  42431  remul01  42604  zaddcom  42661  zmulcom  42665  fidomncyc  42732  evlselvlem  42771  evlselv  42772  fsuppind  42775  mhpind  42779  prjspertr  42790  prjsprellsp  42796  elrfi  42878  nacsfix  42896  fzsplit1nn0  42938  eldioph2  42946  lzenom  42954  irrapxlem3  43008  pellexlem5  43017  pell1234qrne0  43037  pell1234qrmulcl  43039  pell14qrdich  43053  pell1qrge1  43054  pellqrex  43063  reglogltb  43075  reglogleb  43076  rmxypairf1o  43095  rmxycomplete  43101  monotoddzzfi  43126  congadd  43150  congsym  43152  acongrep  43164  jm2.19lem3  43175  jm2.19lem4  43176  jm2.22  43179  jm2.25  43183  expdiophlem1  43205  wepwsolem  43226  kelac1  43247  lmhmfgsplit  43270  pwslnm  43278  hbtlem6  43313  hbt  43314  mon1psubm  43383  deg1mhm  43384  omord2lim  43484  succlg  43512  onmcl  43515  ofoafo  43540  ofoacom  43545  fzunt  43638  fzuntd  43639  fzunt1d  43640  fzuntgd  43641  iunrelexp0  43885  dssmapnvod  44203  gsumws3  44379  gsumws4  44380  mulltgt0  45209  fnchoice  45216  disjrnmpt2  45374  fzisoeu  45490  fsumiunss  45763  climinf  45794  mullimc  45804  mullimcf  45811  stoweidlem14  46200  stoweidlem17  46203  stoweidlem34  46220  stoweidlem50  46236  fourierdlem42  46335  fourierdlem62  46354  fourierdlem71  46363  fourierdlem76  46368  qndenserrnbllem  46480  subsaliuncl  46544  sge0resplit  46592  3f1oss1  47263  2reu8i  47301  addmodne  47532  fundcmpsurinjpreimafv  47596  iccpartigtl  47611  prproropf1olem2  47692  prproropf1olem4  47694  paireqne  47699  prmdvdsfmtnof1lem2  47773  bgoldbtbndlem3  47995  bgoldbtbnd  47997  grimcnv  48076  gricushgr  48105  cycldlenngric  48116  grimedg  48123  grtrimap  48136  isubgr3stgrlem6  48159  isubgr3stgrlem7  48160  isubgr3stgrlem8  48161  isubgr3stgrlem9  48162  grlimfn  48167  gpgedg2iv  48255  gpg5nbgrvtx03starlem2  48257  gpg5nbgrvtx13starlem2  48260  uspgrsprf1  48335  isassintop  48398  2zlidl  48428  2zrngnmrid  48444  rngcinvALTV  48464  funcringcsetcALTV2lem9  48486  ringcinvALTV  48498  funcringcsetclem9ALTV  48509  fldhmsubcALTV  48521  gsumlsscl  48568  lincsum  48617  lindslinindsimp1  48645  lindslinindimp2lem4  48649  lincresunitlem2  48664  elfzolborelfzop1  48707  elbigo2  48740  digexp  48795  dig1  48796  nn0sumshdiglemB  48808  1arymaptf1  48830  2arymaptf1  48841  itcoval1  48851  itcoval2  48852  itcoval3  48853  itcovalsucov  48856  ackvalsuc1mpt  48866  itschlc0xyqsol  48955  brab2dd  49015  dmrnxp  49024  xpco2  49044  initopropd  49430  termopropd  49431  zeroopropd  49432  prcofpropd  49566  thincciso  49640  indthinc  49649  indthincALT  49650  oduoppcciso  49753  lanpropd  49802  ranpropd  49803