Theorem ad2antrl 738

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  simprl  780  simprll  788  simprlr  789  simprl1  1233  simprl2  1234  simprl3  1235  disjxiun  5099  reusv2lem4  5360  axprlem5OLD  5390  fr2nr  5626  somin1  6122  tz7.7  6374  f1oprg  6855  soisores  7313  elovmporab1w  7645  elovmporab1  7646  sorpssi  7714  onint  7775  ordsucelsuc  7804  elxp5  7906  resf1extb  7917  f1oabexg  7924  wemoiso  7956  wemoiso2  7957  el2xptp0  8019  mpof1o2d  8107  frxp2  8126  frxp3  8133  ressuppss  8165  fprlem1  8283  tz7.48lem  8414  oalimcl  8531  oeeui  8574  nnaordex2  8611  oaabs2  8621  omabs  8623  swoer  8712  ralxpmap  8880  pw2f1olem  9055  enfixsn  9060  mapxpen  9117  mapunen  9120  php  9177  unxpdomlem2  9203  unxpdomlem3  9204  isfinite2  9244  fodomfi  9258  domunfican  9268  fissuni  9302  fipreima  9303  indexfi  9305  fsuppsssupp  9329  marypha1lem  9381  marypha2  9387  supmo  9400  infmo  9445  oieu  9489  brwdom2  9523  ixpiunwdom  9540  cantnfval2  9626  cantnfle  9628  cantnflt  9629  cantnf  9650  wemapwe  9654  cnfcom  9657  frrlem15  9717  rankonidlem  9788  r1pwcl  9807  eldju2ndl  9884  eldju2ndr  9885  djuun  9886  infxpenlem  9971  infxpenc2lem1  9977  fseqenlem1  9982  dfac8clem  9990  mappwen  10070  dfac3  10079  dfac5  10087  dfac12lem3  10104  infunsdom  10171  coftr  10232  ssfin4  10269  domfin4  10270  fin23lem26  10284  fin23lem22  10286  fin23lem28  10299  fin23lem32  10303  fin23lem40  10310  isf32lem5  10316  compssiso  10333  isf34lem4  10336  isfin1-3  10345  fin1a2lem13  10371  hsmexlem2  10386  hsmexlem4  10388  zorn2lem1  10455  ttukeylem6  10473  iundom2g  10499  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  11360  addlid  11368  ltord1  11715  divdiv1  11904  divdiv2  11905  conjmul  11910  ltdivmul  12069  ledivmul  12070  lt2mul2div  12072  ltdiv23  12085  lediv23  12086  lediv12a  12087  ledivp1  12096  negfi  12143  nn0nndivcl  12555  nn0ge0div  12644  peano2uz2  12663  peano5uzi  12664  eluzp1m1  12867  qbtwnre  13204  xralrple  13210  xleadd1a  13258  xmulge0  13289  xmulass  13292  xlemul1a  13293  iooshf  13432  divelunit  13500  eluzgtdifelfzo  13735  modadd1  13920  modmul1  13939  seqcl2  14035  seqfveq2  14039  seqid2  14063  seqhomo  14064  seqdistr  14068  mulexpz  14117  leexp2r  14189  expnlbnd2  14249  expmulnbnd  14250  hashmap  14450  hashfun  14452  hashbclem  14467  hashfacen  14469  hashf1lem2  14471  hashf1  14472  ccatsymb  14598  swrdwrdsymb  14678  swrdsb0eq  14679  ccatpfx  14716  swrdswrd  14720  wrdind  14737  wrd2ind  14738  swrdccatin1  14740  swrdccatin2  14744  pfxccatin12lem2  14746  pfxccatin12  14748  swrdccat  14750  repswswrd  14799  0csh0  14808  cshwidxmod  14818  2cshw  14828  cshweqrep  14836  relexp0g  15037  relexpsucnnr  15040  relexpindlem  15078  01sqrexlem1  15271  01sqrexlem6  15276  rlim  15524  rlimclim1  15574  climsup  15699  caurcvg2  15707  caucvgb  15709  iseralt  15714  sumss  15753  fsum2dlem  15799  mptfzshft  15807  modfsummod  15824  o1fsum  15843  incexclem  15868  divrcnv  15884  flo1  15886  fprodrev  16009  fprod2dlem  16012  ruclem6  16269  moddvds  16299  dvdsaddre2b  16343  dvdsflip  16353  addmodlteqALT  16361  nn0o  16419  fldivndvdslt  16452  bitsf1ocnv  16480  bitsf1  16482  sadcaddlem  16493  bezoutlem2  16576  bezoutlem4  16578  lcmgcdlem  16642  prmind2  16721  isprm5  16744  isprm6  16751  prmdvdsncoprmbd  16764  cncongrprm  16766  hashdvds  16812  crth  16815  eulerthlem2  16819  prmdiveq  16823  hashgcdlem  16825  hashgcdeq  16827  iserodd  16873  pclem  16876  pcprendvds2  16879  pcexp  16897  pcneg  16912  pc2dvds  16917  pcmpt  16930  prmpwdvds  16942  pockthg  16944  prmreclem5  16958  4sqlem11  16993  ramub2  17052  ramubcl  17056  ram0  17060  ramub1lem2  17065  ramcl  17067  prmgaplem3  17091  prmgaplem6  17094  setscom  17218  sscpwex  17850  initoeu2  18051  setcinv  18125  funcestrcsetclem9  18182  funcsetcestrclem9  18197  fullsetcestrc  18200  1stfcl  18231  2ndfcl  18232  hofpropd  18301  isacs3lem  18576  isacs4lem  18578  acsmap2d  18589  chnflenfi  18662  subsubmgm  18746  submnd0  18799  mndpsuppss  18801  subsubm  18852  insubm  18854  frmdup1  18900  frmdup3lem  18902  sgrp2nmndlem2  18963  isgrpinv  19037  subsubg  19193  cycsubgcl  19249  conjghm  19291  qusghm  19297  gsumwrev  19408  gsmsymgrfixlem1  19469  symgfixelsi  19477  symgsssg  19509  symgfisg  19510  psgnunilem2  19537  odf1o2  19615  sylow1lem1  19640  odcau  19646  pgpfi  19647  pgpssslw  19656  fislw  19667  efgtlen  19768  efginvrel2  19769  efgrelexlemb  19792  efgredeu  19794  efgcpbllemb  19797  frgpup1  19817  lt6abl  19937  gsum2d  20014  gsum2d2lem  20015  gsum2d2  20016  telgsumfzslem  20030  dmdprdsplit2lem  20089  ablfacrp  20110  pgpfac1lem3  20121  gsummgp0  20368  irredrmul  20478  subsubrng  20615  subsubrg  20650  rngcinv  20689  ringcinv  20723  fldhmsubc  20836  islss4  21031  lspextmo  21125  lspsnat  21217  prmirredlem  21526  znf1o  21605  znidomb  21615  frgpcyg  21627  psgnghm  21634  psgndiflemB  21654  frlmlbs  21851  frlmup1  21852  lindfind  21870  islindf3  21880  lindfmm  21881  issubassa3  21920  resspsradd  22028  resspsrmul  22029  psdmul  22233  coe1tmmul2  22341  pf1ind  22420  mamulid  22503  mat1dimelbas  22533  mdetdiaglem  22660  mdetralt2  22671  mndifsplit  22698  smadiadetglem2  22734  1elcpmat  22777  pmatcollpw3lem  22845  chfacfisf  22916  chfacfisfcpmat  22917  chfacffsupp  22918  chfacfscmulfsupp  22921  chfacfscmulgsum  22922  chfacfpmmulfsupp  22925  chfacfpmmulgsum  22926  chfacfpmmulgsum2  22927  cayhamlem1  22928  cpmadugsumlemF  22938  cayleyhamilton1  22954  tgcl  23031  pptbas  23070  clsval2  23112  mretopd  23154  lmbr2  23321  cncls2  23335  nrmsep  23419  regsep2  23438  cmpsublem  23461  cmpsub  23462  tgcmp  23463  uncmp  23465  hauscmplem  23468  iunconnlem  23489  1stcrest  23515  2ndcctbss  23517  2ndcsep  23521  dis2ndc  23522  hausllycmp  23556  dislly  23559  kgentopon  23600  1stckgen  23616  kgencn3  23620  ptpjpre1  23633  ptbasin  23639  ptpjopn  23674  dfac14  23680  ptcnplem  23683  txcn  23688  txindis  23696  txdis1cn  23697  ptrescn  23701  txcmplem1  23703  txcmp  23705  txhaus  23709  txlm  23710  tx1stc  23712  txkgen  23714  xkococn  23722  qtopcn  23776  kqreglem1  23803  kqreglem2  23804  kqnrmlem1  23805  kqnrmlem2  23806  hmeoimaf1o  23832  reghmph  23855  nrmhmph  23856  txhmeo  23865  ptuncnv  23869  filconn  23945  fbasrn  23946  fmfnfmlem2  24017  flimfnfcls  24090  cnpfcfi  24102  alexsublem  24106  alexsubALTlem2  24110  alexsubALTlem3  24111  alexsubALTlem4  24112  alexsubALT  24113  ptcmplem3  24116  cnextfval  24124  tsmsxp  24217  imasdsf1olem  24435  bl2in  24462  blssps  24486  blss  24487  blssexps  24488  blssex  24489  blcld  24567  stdbdxmet  24577  met1stc  24583  prdsxmslem2  24591  metcnp3  24602  metcnpi3  24608  txmetcnp  24609  nmo0  24797  nmoid  24804  icccmplem1  24885  icccmp  24888  xrge0tsms  24897  metdseq0  24917  cnheiborlem  25018  cnheibor  25019  cnllycmp  25020  pcoval2  25080  cmetcaulem  25352  iscmet3lem1  25355  iscmet3lem2  25356  equivcau  25364  lmcau  25377  cncmet  25386  ivthlem2  25516  ivthlem3  25517  ovoliunlem2  25567  ovolscalem2  25578  uniioombl  25653  dyaddisj  25660  opnmbllem  25665  volivth  25671  ismbfd  25703  ismbf3d  25718  mbfimaopnlem  25719  mbfinf  25729  itg1addlem4  25763  mbfi1fseqlem1  25779  mbfi1fseqlem3  25781  mbfi1fseqlem4  25782  mbfi1fseqlem5  25783  mbfi1fseqlem6  25784  itg2seq  25806  itg2lea  25808  itg2split  25813  itg2cnlem1  25825  bddiblnc  25906  limciun  25958  dvmptfsum  26039  rolle  26054  c1lip1  26061  dvcnvrelem1  26081  dvcnvre  26083  dvcvx  26084  itgsubst  26113  tdeglem4  26122  mdegmullem  26140  plyco0  26254  coemullem  26312  dgreq0  26327  dgrmul  26332  dgrco  26337  elqaalem2  26386  aannenlem1  26394  aaliou3lem9  26416  ulmres  26453  ulmshftlem  26454  angneg  26870  dcubic  26913  cxploglim  27044  cxploglim2  27045  scvxcvx  27052  lgamgulmlem5  27099  lgamcvg2  27121  ftalem2  27140  basellem3  27149  basellem4  27150  sqff1o  27248  fsumdvdsdiaglem  27249  dvdsflsumcom  27254  mpodvdsmulf1o  27260  dvdsmulf1o  27262  fsumvma2  27280  logfac2  27283  logfacrlim  27290  logexprlim  27291  dchrelbasd  27305  lgsne0  27401  lgsqrlem2  27413  lgsqrmodndvds  27419  gausslemma2dlem1a  27431  lgseisenlem2  27442  lgsquadlem1  27446  lgsquadlem2  27447  lgsquadlem3  27448  lgsquad2lem2  27451  2sqlem8  27492  2sqlem11  27495  2sqreultlem  27513  2sqreunnltlem  27516  chpo1ubb  27547  vmadivsum  27548  rplogsumlem2  27551  rpvmasumlem  27553  dchrmusum2  27560  dchrvmasumlem1  27561  dchrisum0fno1  27577  dchrisum0re  27579  dchrisum0lem1  27582  dchrisum0lem2  27584  dchrisum0lem3  27585  dchrisum0  27586  mulogsumlem  27597  mulog2sumlem2  27601  vmalogdivsum2  27604  logsqvma  27608  log2sumbnd  27610  selberglem3  27613  selberg  27614  selberg2lem  27616  selberg2b  27618  selberg3lem2  27624  pntrmax  27630  pntrsumo1  27631  pntlemn  27666  pntlemp  27676  qabvle  27691  ostthlem1  27693  ostthlem2  27694  ostth2lem2  27700  ostth3  27704  ltsres  27728  nosupno  27769  nosupbnd2  27782  noinfno  27784  noinfbnd2  27797  etaslts  27888  cuteq1  27912  addsproplem2  28065  mulsval  28204  precsexlem11  28312  n0fincut  28450  zmulscld  28492  bdayfinbndlem1  28562  idmot  28708  plngval  28986  brbtwn2  29108  colinearalglem4  29112  colinearalg  29113  ax5seglem9  29140  axpaschlem  29143  axcontlem2  29168  axcontlem7  29173  axcontlem8  29174  eengtrkg  29189  upgr1eopALT  29320  uspgredg2vlem  29426  subumgr  29491  nbgr0edglem  29559  edgnbusgreu  29570  nb3grprlem1  29583  wlkl1loop  29840  pthdivtx  29929  usgr2pth  29966  crctcshwlkn0  30023  wlklnwwlkln1  30070  wwlksnext  30095  clwwlkccatlem  30193  clwlkclwwlklem2a  30202  clwwlkinwwlk  30244  clwwlkn1loopb  30247  clwwlkf  30251  wwlksext2clwwlk  30261  wwlksubclwwlk  30262  clwwlknscsh  30266  clwwlknon1  30301  clwwlknonex2e  30314  1conngr  30398  n4cyclfrgr  30495  numclwwlk2lem1lem  30546  2clwwlk2clwwlk  30554  numclwwlk1lem2f1  30561  numclwlk1lem1  30573  numclwwlk2lem1  30580  numclwlk2lem2f  30581  numclwwlk7  30595  frgrogt3nreg  30601  grpoidinvlem1  30709  grpoidinvlem3  30711  grporcan  30723  nmlnoubi  31001  blocnilem  31009  ipblnfi  31060  htthlem  31122  ocsh  31488  shmodsi  31594  pjhthlem2  31597  5oalem2  31860  eigposi  32041  nmopub2tALT  32114  nmfnleub2  32131  nmcexi  32231  nmopcoi  32300  kbass3  32323  mdslmd1lem1  32530  mdslmd1lem2  32531  chirredlem2  32596  chirredlem4  32598  mdsymlem3  32610  mdsymlem5  32612  sumdmdii  32620  sumdmdlem  32623  sumdmdlem2  32624  foresf1o  32705  disjxpin  32790  1stpreimas  32910  resf1o  32934  nn0xmulclb  32975  wrdt2ind  33133  xrge0tsmsd  33255  gsumvsca1  33408  gsumvsca2  33409  islinds5  33555  1arithidomlem2  33734  mplvrpmmhm  33845  irngnzply1  33990  mdetpmtr1  34122  mdetpmtr2  34123  pstmxmet  34196  qqhghm  34287  qqhrhm  34288  esumpcvgval  34377  volmeas  34530  imambfm  34561  dya2iocnrect  34580  oddpwdc  34653  sseqf  34691  orvcgteel  34767  orvclteel  34772  ballotlemsf1o  34813  bnj1110  35279  bnj1118  35281  f1resveqaeq  35381  txpconn  35587  connpconn  35590  cnllysconn  35600  rellysconn  35606  cvmsss2  35629  cvmlift2lem9  35666  satf00  35729  fmlasuc  35741  mrsubfval  35863  mppsval  35927  dfon2lem6  36141  wzel  36177  ifscgr  36399  cgrxfr  36410  btwnconn1lem5  36446  btwnconn1lem6  36447  btwnconn1lem12  36453  brsegle  36463  finminlem  36683  nn0prpwlem  36687  fnessref  36722  refssfne  36723  neibastop1  36724  topjoin  36730  fnemeet2  36732  weiunse  36833  mh-inf3f1  36906  bj-prmoore  37610  bj-finsumval0  37782  topdifinffinlem  37846  lindsadd  38117  matunitlindflem2  38121  poimirlem28  38152  poimirlem32  38156  opnmbllem0  38160  mblfinlem1  38161  mblfinlem4  38164  ismblfin  38165  mbfresfi  38170  itg2addnclem  38175  itg2addnclem3  38177  itg2addnc  38178  unirep  38218  frinfm  38239  sdclem2  38246  geomcau  38263  istotbnd3  38275  sstotbnd2  38278  sstotbnd  38279  sstotbnd3  38280  totbndbnd  38293  cntotbnd  38300  ismtyres  38312  heibor1lem  38313  heiborlem1  38315  heiborlem8  38322  ismndo1  38377  isdivrngo  38454  unichnidl  38535  erimeq2  39267  cvlcvr1  39968  ishlat3N  39983  llnmlplnN  40168  islvol2aN  40221  4atlem4c  40230  4atlem4d  40231  isline2  40403  isline3  40405  linepsubclN  40580  lhpexle3lem  40640  lhpjat2  40650  cdlemd4  40830  cdleme0cq  40844  cdleme32fva  41066  cdleme32fvaw  41068  tendo0mul  41455  tendo0mulr  41456  diameetN  41685  dvhvaddcl  41724  dvhvaddcomN  41725  cdlemm10N  41747  dvadiaN  41757  djavalN  41764  dihvalcqat  41868  dihopelvalcpre  41877  djhval  42027  dihjat1lem  42057  sticksstones11  42778  sticksstones22  42790  remul01  43021  zaddcom  43091  zmulcom  43095  fidomncyc  43158  evlselvlem  43175  evlselv  43176  fsuppind  43177  mhpind  43181  prjspertr  43192  prjsprellsp  43198  elrfi  43280  nacsfix  43298  fzsplit1nn0  43340  eldioph2  43348  lzenom  43356  irrapxlem3  43406  pellexlem5  43415  pell1234qrne0  43435  pell1234qrmulcl  43437  pell14qrdich  43451  pell1qrge1  43452  pellqrex  43461  reglogltb  43473  reglogleb  43474  rmxypairf1o  43493  rmxycomplete  43499  monotoddzzfi  43524  congadd  43548  congsym  43550  acongrep  43562  jm2.19lem3  43573  jm2.19lem4  43574  jm2.22  43577  jm2.25  43581  expdiophlem1  43603  wepwsolem  43624  kelac1  43645  lmhmfgsplit  43668  pwslnm  43676  hbtlem6  43711  hbt  43712  mon1psubm  43781  deg1mhm  43782  omord2lim  43882  succlg  43910  onmcl  43913  ofoafo  43938  ofoacom  43943  fzunt  44036  fzuntd  44037  fzunt1d  44038  fzuntgd  44039  iunrelexp0  44283  dssmapnvod  44601  gsumws3  44777  gsumws4  44778  mulltgt0  45607  fnchoice  45614  disjrnmpt2  45771  fzisoeu  45884  fsumiunss  46156  climinf  46187  mullimc  46197  mullimcf  46204  stoweidlem14  46593  stoweidlem17  46596  stoweidlem34  46613  stoweidlem50  46629  fourierdlem42  46728  fourierdlem62  46747  fourierdlem71  46756  fourierdlem76  46761  qndenserrnbllem  46873  subsaliuncl  46937  sge0resplit  46985  3f1oss1  47674  2reu8i  47712  addmodne  47949  fundcmpsurinjpreimafv  48019  iccpartigtl  48034  prproropf1olem2  48115  prproropf1olem4  48117  paireqne  48122  prmdvdsfmtnof1lem2  48199  nprmdvdsfacm1  48238  bgoldbtbndlem3  48434  bgoldbtbnd  48436  grimcnv  48515  gricushgr  48544  cycldlenngric  48555  grimedg  48562  grtrimap  48575  isubgr3stgrlem6  48598  isubgr3stgrlem7  48599  isubgr3stgrlem8  48600  isubgr3stgrlem9  48601  grlimfn  48606  gpgedg2iv  48694  gpg5nbgrvtx03starlem2  48696  gpg5nbgrvtx13starlem2  48699  uspgrsprf1  48774  isassintop  48837  2zlidl  48867  2zrngnmrid  48883  rngcinvALTV  48903  funcringcsetcALTV2lem9  48925  ringcinvALTV  48937  funcringcsetclem9ALTV  48948  fldhmsubcALTV  48960  gsumlsscl  49007  lincsum  49056  lindslinindsimp1  49084  lindslinindimp2lem4  49088  lincresunitlem2  49103  elfzolborelfzop1  49146  elbigo2  49179  digexp  49234  dig1  49235  nn0sumshdiglemB  49247  1arymaptf1  49269  2arymaptf1  49280  itcoval1  49290  itcoval2  49291  itcoval3  49292  itcovalsucov  49295  ackvalsuc1mpt  49305  itschlc0xyqsol  49394  brab2dd  49454  dmrnxp  49463  xpco2  49483  initopropd  49869  termopropd  49870  zeroopropd  49871  prcofpropd  50005  thincciso  50079  indthinc  50088  indthincALT  50089  oduoppcciso  50192  lanpropd  50241  ranpropd  50242