Theorem ad2antrl 724

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 713	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 206  df-an 396

This theorem is referenced by:  simprl  767  simprll  775  simprlr  776  simprl1  1216  simprl2  1217  simprl3  1218  disjxiun  5067  reusv2lem4  5319  axprlem5  5345  fr2nr  5558  somin1  6027  tz7.7  6277  f1oprg  6744  soisores  7178  elovmporab1w  7494  elovmporab1  7495  sorpssi  7560  onint  7617  ordsucelsuc  7644  elxp5  7744  wemoiso  7789  wemoiso2  7790  el2xptp0  7851  ressuppss  7970  fprlem1  8087  tz7.48lem  8242  oalimcl  8353  oeeui  8395  oaabs2  8439  omabs  8441  swoer  8486  ralxpmap  8642  pw2f1olem  8816  enfixsn  8821  mapxpen  8879  mapunen  8882  unxpdomlem2  8957  unxpdomlem3  8958  findcard3  8987  isfinite2  9002  domunfican  9017  fodomfi  9022  fissuni  9054  fipreima  9055  indexfi  9057  fsuppsssupp  9074  marypha1lem  9122  marypha2  9128  supmo  9141  infmo  9184  oieu  9228  brwdom2  9262  ixpiunwdom  9279  cantnfval2  9357  cantnfle  9359  cantnflt  9360  cantnf  9381  wemapwe  9385  cnfcom  9388  trpredmintr  9409  frrlem15  9446  rankonidlem  9517  r1pwcl  9536  eldju2ndl  9613  eldju2ndr  9614  djuun  9615  infxpenlem  9700  infxpenc2lem1  9706  fseqenlem1  9711  dfac8clem  9719  mappwen  9799  dfac3  9808  dfac5  9815  dfac12lem3  9832  infunsdom  9901  coftr  9960  ssfin4  9997  domfin4  9998  fin23lem26  10012  fin23lem22  10014  fin23lem28  10027  fin23lem32  10031  fin23lem40  10038  isf32lem5  10044  compssiso  10061  isf34lem4  10064  isfin1-3  10073  fin1a2lem13  10099  hsmexlem2  10114  hsmexlem4  10116  zorn2lem1  10183  ttukeylem6  10201  iundom2g  10227  konigthlem  10255  pwcfsdom  10270  fpwwe2lem11  10328  fpwwe2  10330  pwfseqlem3  10347  winalim2  10383  r1wunlim  10424  inttsk  10461  inar1  10462  grur1  10507  nqereq  10622  ltexprlem7  10729  prlem936  10734  00id  11080  addid2  11088  ltord1  11431  divdiv1  11616  divdiv2  11617  conjmul  11622  ltdivmul  11780  ledivmul  11781  lt2mul2div  11783  ltdiv23  11796  lediv23  11797  lediv12a  11798  ledivp1  11807  negfi  11854  nn0nndivcl  12234  nn0ge0div  12319  peano2uz2  12338  peano5uzi  12339  eluzp1m1  12537  qbtwnre  12862  xralrple  12868  xleadd1a  12916  xmulge0  12947  xmulass  12950  xlemul1a  12951  iooshf  13087  divelunit  13155  eluzgtdifelfzo  13377  modadd1  13556  modmul1  13572  seqcl2  13669  seqfveq2  13673  seqid2  13697  seqhomo  13698  seqdistr  13702  mulexpz  13751  leexp2r  13820  expnlbnd2  13877  expmulnbnd  13878  hashmap  14078  hashfun  14080  hashbclem  14092  hashfacen  14094  hashfacenOLD  14095  hashf1lem2  14098  hashf1  14099  ccatsymb  14215  swrdwrdsymb  14303  swrdsb0eq  14304  ccatpfx  14342  swrdswrd  14346  wrdind  14363  wrd2ind  14364  swrdccatin1  14366  swrdccatin2  14370  pfxccatin12lem2  14372  pfxccatin12  14374  swrdccat  14376  repswswrd  14425  0csh0  14434  cshwidxmod  14444  2cshw  14454  cshweqrep  14462  relexp0g  14661  relexpsucnnr  14664  relexpindlem  14702  sqrlem1  14882  sqrlem6  14887  rlim  15132  rlimclim1  15182  climsup  15309  caurcvg2  15317  caucvgb  15319  iseralt  15324  sumss  15364  fsum2dlem  15410  mptfzshft  15418  modfsummod  15434  o1fsum  15453  incexclem  15476  divrcnv  15492  flo1  15494  fprodrev  15615  fprod2dlem  15618  ruclem6  15872  moddvds  15902  dvdsaddre2b  15944  dvdsflip  15954  addmodlteqALT  15962  nn0o  16020  fldivndvdslt  16051  bitsf1ocnv  16079  bitsf1  16081  sadcaddlem  16092  bezoutlem2  16176  bezoutlem4  16178  lcmgcdlem  16239  prmind2  16318  isprm5  16340  isprm6  16347  prmdvdsncoprmbd  16359  cncongrprm  16361  hashdvds  16404  crth  16407  eulerthlem2  16411  prmdiveq  16415  hashgcdlem  16417  hashgcdeq  16418  iserodd  16464  pclem  16467  pcprendvds2  16470  pcexp  16488  pcneg  16503  pc2dvds  16508  pcmpt  16521  prmpwdvds  16533  pockthg  16535  prmreclem5  16549  4sqlem11  16584  ramub2  16643  ramubcl  16647  ram0  16651  ramub1lem2  16656  ramcl  16658  prmgaplem3  16682  prmgaplem6  16685  setscom  16809  sscpwex  17444  initoeu2  17647  setcinv  17721  funcestrcsetclem9  17781  funcsetcestrclem9  17796  fullsetcestrc  17799  1stfcl  17830  2ndfcl  17831  hofpropd  17901  isacs3lem  18175  isacs4lem  18177  acsmap2d  18188  submnd0  18329  subsubm  18370  insubm  18372  frmdup1  18418  frmdup3lem  18420  sgrp2nmndlem2  18478  isgrpinv  18547  subsubg  18693  cycsubgcl  18740  conjghm  18780  qusghm  18786  gsumwrev  18888  gsmsymgrfixlem1  18950  symgfixelsi  18958  symgsssg  18990  symgfisg  18991  psgnunilem2  19018  odf1o2  19093  sylow1lem1  19118  odcau  19124  pgpfi  19125  pgpssslw  19134  fislw  19145  efgtlen  19247  efginvrel2  19248  efgrelexlemb  19271  efgredeu  19273  efgcpbllemb  19276  frgpup1  19296  cygablOLD  19407  lt6abl  19411  gsum2d  19488  gsum2d2lem  19489  gsum2d2  19490  telgsumfzslem  19504  dmdprdsplit2lem  19563  ablfacrp  19584  pgpfac1lem3  19595  gsummgp0  19762  irredrmul  19864  subsubrg  19965  islss4  20139  lspextmo  20233  lspsnat  20322  prmirredlem  20606  znf1o  20671  znidomb  20681  frgpcyg  20693  psgnghm  20697  psgndiflemB  20717  frlmlbs  20914  frlmup1  20915  lindfind  20933  islindf3  20943  lindfmm  20944  issubassa3  20982  resspsradd  21095  resspsrmul  21096  coe1tmmul2  21357  pf1ind  21431  mamulid  21498  mat1dimelbas  21528  mdetdiaglem  21655  mdetralt2  21666  mndifsplit  21693  smadiadetglem2  21729  1elcpmat  21772  pmatcollpw3lem  21840  chfacfisf  21911  chfacfisfcpmat  21912  chfacffsupp  21913  chfacfscmulfsupp  21916  chfacfscmulgsum  21917  chfacfpmmulfsupp  21920  chfacfpmmulgsum  21921  chfacfpmmulgsum2  21922  cayhamlem1  21923  cpmadugsumlemF  21933  cayleyhamilton1  21949  tgcl  22027  pptbas  22066  clsval2  22109  mretopd  22151  lmbr2  22318  cncls2  22332  nrmsep  22416  regsep2  22435  cmpsublem  22458  cmpsub  22459  tgcmp  22460  uncmp  22462  hauscmplem  22465  iunconnlem  22486  1stcrest  22512  2ndcctbss  22514  2ndcsep  22518  dis2ndc  22519  hausllycmp  22553  dislly  22556  kgentopon  22597  1stckgen  22613  kgencn3  22617  ptpjpre1  22630  ptbasin  22636  ptpjopn  22671  dfac14  22677  ptcnplem  22680  txcn  22685  txindis  22693  txdis1cn  22694  ptrescn  22698  txcmplem1  22700  txcmp  22702  txhaus  22706  txlm  22707  tx1stc  22709  txkgen  22711  xkococn  22719  qtopcn  22773  kqreglem1  22800  kqreglem2  22801  kqnrmlem1  22802  kqnrmlem2  22803  hmeoimaf1o  22829  reghmph  22852  nrmhmph  22853  txhmeo  22862  ptuncnv  22866  filconn  22942  fbasrn  22943  fmfnfmlem2  23014  flimfnfcls  23087  cnpfcfi  23099  alexsublem  23103  alexsubALTlem2  23107  alexsubALTlem3  23108  alexsubALTlem4  23109  alexsubALT  23110  ptcmplem3  23113  cnextfval  23121  tsmsxp  23214  imasdsf1olem  23434  bl2in  23461  blssps  23485  blss  23486  blssexps  23487  blssex  23488  blcld  23567  stdbdxmet  23577  met1stc  23583  prdsxmslem2  23591  metcnp3  23602  metcnpi3  23608  txmetcnp  23609  nmo0  23805  nmoid  23812  icccmplem1  23891  icccmp  23894  xrge0tsms  23903  metdseq0  23923  cnheiborlem  24023  cnheibor  24024  cnllycmp  24025  pcoval2  24085  cmetcaulem  24357  iscmet3lem1  24360  iscmet3lem2  24361  equivcau  24369  lmcau  24382  cncmet  24391  ivthlem2  24521  ivthlem3  24522  ovoliunlem2  24572  ovolscalem2  24583  uniioombl  24658  dyaddisj  24665  opnmbllem  24670  volivth  24676  ismbfd  24708  ismbf3d  24723  mbfimaopnlem  24724  mbfinf  24734  itg1addlem4  24768  itg1addlem4OLD  24769  mbfi1fseqlem1  24785  mbfi1fseqlem3  24787  mbfi1fseqlem4  24788  mbfi1fseqlem5  24789  mbfi1fseqlem6  24790  itg2seq  24812  itg2lea  24814  itg2split  24819  itg2cnlem1  24831  bddiblnc  24911  limciun  24963  dvmptfsum  25044  rolle  25059  c1lip1  25066  dvcnvrelem1  25086  dvcnvre  25088  dvcvx  25089  itgsubst  25118  tdeglem4  25129  tdeglem4OLD  25130  mdegmullem  25148  plyco0  25258  coemullem  25316  dgreq0  25331  dgrmul  25336  dgrco  25341  elqaalem2  25385  aannenlem1  25393  aaliou3lem9  25415  ulmres  25452  ulmshftlem  25453  angneg  25858  dcubic  25901  cxploglim  26032  cxploglim2  26033  scvxcvx  26040  lgamgulmlem5  26087  lgamcvg2  26109  ftalem2  26128  basellem3  26137  basellem4  26138  sqff1o  26236  fsumdvdsdiaglem  26237  dvdsflsumcom  26242  dvdsmulf1o  26248  fsumvma2  26267  logfac2  26270  logfacrlim  26277  logexprlim  26278  dchrelbasd  26292  lgsne0  26388  lgsqrlem2  26400  lgsqrmodndvds  26406  gausslemma2dlem1a  26418  lgseisenlem2  26429  lgsquadlem1  26433  lgsquadlem2  26434  lgsquadlem3  26435  lgsquad2lem2  26438  2sqlem8  26479  2sqlem11  26482  2sqreultlem  26500  2sqreunnltlem  26503  chpo1ubb  26534  vmadivsum  26535  rplogsumlem2  26538  rpvmasumlem  26540  dchrmusum2  26547  dchrvmasumlem1  26548  dchrisum0fno1  26564  dchrisum0re  26566  dchrisum0lem1  26569  dchrisum0lem2  26571  dchrisum0lem3  26572  dchrisum0  26573  mulogsumlem  26584  mulog2sumlem2  26588  vmalogdivsum2  26591  logsqvma  26595  log2sumbnd  26597  selberglem3  26600  selberg  26601  selberg2lem  26603  selberg2b  26605  selberg3lem2  26611  pntrmax  26617  pntrsumo1  26618  pntlemn  26653  pntlemp  26663  qabvle  26678  ostthlem1  26680  ostthlem2  26681  ostth2lem2  26687  ostth3  26691  idmot  26802  brbtwn2  27176  colinearalglem4  27180  colinearalg  27181  ax5seglem9  27208  axpaschlem  27211  axcontlem2  27236  axcontlem7  27241  axcontlem8  27242  eengtrkg  27257  upgr1eopALT  27390  uspgredg2vlem  27493  subumgr  27558  nbgr0vtxlem  27625  edgnbusgreu  27637  nb3grprlem1  27650  wlkl1loop  27907  pthdivtx  27998  usgr2pth  28033  crctcshwlkn0  28087  wlklnwwlkln1  28134  wwlksnext  28159  clwwlkccatlem  28254  clwlkclwwlklem2a  28263  clwwlkinwwlk  28305  clwwlkn1loopb  28308  clwwlkf  28312  wwlksext2clwwlk  28322  wwlksubclwwlk  28323  clwwlknscsh  28327  clwwlknon1  28362  clwwlknonex2e  28375  1conngr  28459  n4cyclfrgr  28556  numclwwlk2lem1lem  28607  2clwwlk2clwwlk  28615  numclwwlk1lem2f1  28622  numclwlk1lem1  28634  numclwwlk2lem1  28641  numclwlk2lem2f  28642  numclwwlk7  28656  frgrogt3nreg  28662  grpoidinvlem1  28767  grpoidinvlem3  28769  grporcan  28781  nmlnoubi  29059  blocnilem  29067  ipblnfi  29118  htthlem  29180  ocsh  29546  shmodsi  29652  pjhthlem2  29655  5oalem2  29918  eigposi  30099  nmopub2tALT  30172  nmfnleub2  30189  nmcexi  30289  nmopcoi  30358  kbass3  30381  mdslmd1lem1  30588  mdslmd1lem2  30589  chirredlem2  30654  chirredlem4  30656  mdsymlem3  30668  mdsymlem5  30670  sumdmdii  30678  sumdmdlem  30681  sumdmdlem2  30682  foresf1o  30751  disjxpin  30828  1stpreimas  30940  resf1o  30967  nn0xmulclb  30996  wrdt2ind  31127  xrge0tsmsd  31219  gsumvsca1  31381  gsumvsca2  31382  islinds5  31465  mdetpmtr1  31675  mdetpmtr2  31676  pstmxmet  31749  qqhghm  31838  qqhrhm  31839  esumpcvgval  31946  volmeas  32099  imambfm  32129  dya2iocnrect  32148  oddpwdc  32221  sseqf  32259  orvcgteel  32334  orvclteel  32339  ballotlemsf1o  32380  bnj1110  32862  bnj1118  32864  f1resveqaeq  32957  txpconn  33094  connpconn  33097  cnllysconn  33107  rellysconn  33113  cvmsss2  33136  cvmlift2lem9  33173  satf00  33236  fmlasuc  33248  mrsubfval  33370  mppsval  33434  dfon2lem6  33670  frxp2  33718  poxp3  33723  frxp3  33724  wzel  33745  sltres  33792  nosupno  33833  nosupbnd2  33846  noinfno  33848  noinfbnd2  33861  etasslt  33934  ifscgr  34273  cgrxfr  34284  btwnconn1lem5  34320  btwnconn1lem6  34321  btwnconn1lem12  34327  brsegle  34337  finminlem  34434  nn0prpwlem  34438  fnessref  34473  refssfne  34474  neibastop1  34475  topjoin  34481  fnemeet2  34483  bj-prmoore  35213  bj-finsumval0  35383  topdifinffinlem  35445  lindsadd  35697  matunitlindflem2  35701  poimirlem28  35732  poimirlem32  35736  opnmbllem0  35740  mblfinlem1  35741  mblfinlem4  35744  ismblfin  35745  mbfresfi  35750  itg2addnclem  35755  itg2addnclem3  35757  itg2addnc  35758  unirep  35798  frinfm  35820  sdclem2  35827  geomcau  35844  istotbnd3  35856  sstotbnd2  35859  sstotbnd  35860  sstotbnd3  35861  totbndbnd  35874  cntotbnd  35881  ismtyres  35893  heibor1lem  35894  heiborlem1  35896  heiborlem8  35903  ismndo1  35958  isdivrngo  36035  unichnidl  36116  erim2  36716  cvlcvr1  37280  ishlat3N  37295  llnmlplnN  37480  islvol2aN  37533  4atlem4c  37542  4atlem4d  37543  isline2  37715  isline3  37717  linepsubclN  37892  lhpexle3lem  37952  lhpjat2  37962  cdlemd4  38142  cdleme0cq  38156  cdleme32fva  38378  cdleme32fvaw  38380  tendo0mul  38767  tendo0mulr  38768  diameetN  38997  dvhvaddcl  39036  dvhvaddcomN  39037  cdlemm10N  39059  dvadiaN  39069  djavalN  39076  dihvalcqat  39180  dihopelvalcpre  39189  djhval  39339  dihjat1lem  39369  sticksstones11  40040  sticksstones22  40052  metakunt15  40067  metakunt16  40068  evlsbagval  40198  fsuppind  40202  mhpind  40206  mhphf  40208  remul01  40311  prjspertr  40365  prjsprellsp  40371  elrfi  40432  nacsfix  40450  fzsplit1nn0  40492  eldioph2  40500  lzenom  40508  irrapxlem3  40562  pellexlem5  40571  pell1234qrne0  40591  pell1234qrmulcl  40593  pell14qrdich  40607  pell1qrge1  40608  pellqrex  40617  reglogltb  40629  reglogleb  40630  rmxypairf1o  40649  rmxycomplete  40655  monotoddzzfi  40680  congadd  40704  congsym  40706  acongrep  40718  jm2.19lem3  40729  jm2.19lem4  40730  jm2.22  40733  jm2.25  40737  expdiophlem1  40759  wepwsolem  40783  kelac1  40804  lmhmfgsplit  40827  pwslnm  40835  hbtlem6  40870  hbt  40871  mon1psubm  40947  deg1mhm  40948  iunrelexp0  41199  dssmapnvod  41517  gsumws3  41696  gsumws4  41697  mulltgt0  42454  fnchoice  42461  disjrnmpt2  42615  fzisoeu  42729  fsumiunss  43006  climinf  43037  mullimc  43047  mullimcf  43054  stoweidlem14  43445  stoweidlem17  43448  stoweidlem34  43465  stoweidlem50  43481  fourierdlem42  43580  fourierdlem62  43599  fourierdlem71  43608  fourierdlem76  43613  qndenserrnbllem  43725  subsaliuncl  43787  sge0resplit  43834  2reu8i  44492  fundcmpsurinjpreimafv  44748  iccpartigtl  44763  prproropf1olem2  44844  prproropf1olem4  44846  paireqne  44851  prmdvdsfmtnof1lem2  44925  bgoldbtbndlem3  45147  bgoldbtbnd  45149  isomushgr  45166  isomuspgrlem2c  45170  uspgrsprf1  45197  subsubmgm  45239  isassintop  45292  2zlidl  45380  2zrngnmrid  45396  rngcinv  45427  rngcinvALTV  45439  ringcinv  45478  funcringcsetcALTV2lem9  45490  ringcinvALTV  45502  funcringcsetclem9ALTV  45513  fldhmsubc  45530  fldhmsubcALTV  45548  mndpsuppss  45595  gsumlsscl  45607  lincsum  45658  lindslinindsimp1  45686  lindslinindimp2lem4  45690  lincresunitlem2  45705  elfzolborelfzop1  45748  elbigo2  45786  digexp  45841  dig1  45842  nn0sumshdiglemB  45854  1arymaptf1  45876  2arymaptf1  45887  itcoval1  45897  itcoval2  45898  itcoval3  45899  itcovalsucov  45902  ackvalsuc1mpt  45912  itschlc0xyqsol  46001  thincciso  46218  indthinc  46221  indthincALT  46222