Theorem ad2antrl 729

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 718	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  771  simprll  779  simprlr  780  simprl1  1220  simprl2  1221  simprl3  1222  disjxiun  5097  reusv2lem4  5350  axprlem5OLD  5379  fr2nr  5611  somin1  6100  tz7.7  6353  f1oprg  6830  soisores  7285  elovmporab1w  7617  elovmporab1  7618  sorpssi  7686  onint  7747  ordsucelsuc  7776  elxp5  7877  resf1extb  7888  f1oabexg  7896  wemoiso  7929  wemoiso2  7930  el2xptp0  7992  frxp2  8098  frxp3  8105  ressuppss  8137  fprlem1  8254  tz7.48lem  8384  oalimcl  8499  oeeui  8542  nnaordex2  8579  oaabs2  8589  omabs  8591  swoer  8679  ralxpmap  8848  pw2f1olem  9023  enfixsn  9028  mapxpen  9085  mapunen  9088  php  9145  unxpdomlem2  9171  unxpdomlem3  9172  isfinite2  9212  fodomfi  9226  domunfican  9236  fodomfiOLD  9244  fissuni  9271  fipreima  9272  indexfi  9274  fsuppsssupp  9298  marypha1lem  9350  marypha2  9356  supmo  9369  infmo  9414  oieu  9458  brwdom2  9492  ixpiunwdom  9509  cantnfval2  9592  cantnfle  9594  cantnflt  9595  cantnf  9616  wemapwe  9620  cnfcom  9623  frrlem15  9683  rankonidlem  9754  r1pwcl  9773  eldju2ndl  9850  eldju2ndr  9851  djuun  9852  infxpenlem  9937  infxpenc2lem1  9943  fseqenlem1  9948  dfac8clem  9956  mappwen  10036  dfac3  10045  dfac5  10053  dfac12lem3  10070  infunsdom  10137  coftr  10197  ssfin4  10234  domfin4  10235  fin23lem26  10249  fin23lem22  10251  fin23lem28  10264  fin23lem32  10268  fin23lem40  10275  isf32lem5  10281  compssiso  10298  isf34lem4  10301  isfin1-3  10310  fin1a2lem13  10336  hsmexlem2  10351  hsmexlem4  10353  zorn2lem1  10420  ttukeylem6  10438  iundom2g  10464  konigthlem  10493  pwcfsdom  10508  fpwwe2lem11  10566  fpwwe2  10568  pwfseqlem3  10585  winalim2  10621  r1wunlim  10662  inttsk  10699  inar1  10700  grur1  10745  nqereq  10860  ltexprlem7  10967  prlem936  10972  00id  11322  addlid  11330  ltord1  11677  divdiv1  11866  divdiv2  11867  conjmul  11872  ltdivmul  12031  ledivmul  12032  lt2mul2div  12034  ltdiv23  12047  lediv23  12048  lediv12a  12049  ledivp1  12058  negfi  12105  nn0nndivcl  12487  nn0ge0div  12575  peano2uz2  12594  peano5uzi  12595  eluzp1m1  12791  qbtwnre  13128  xralrple  13134  xleadd1a  13182  xmulge0  13213  xmulass  13216  xlemul1a  13217  iooshf  13356  divelunit  13424  eluzgtdifelfzo  13657  modadd1  13842  modmul1  13861  seqcl2  13957  seqfveq2  13961  seqid2  13985  seqhomo  13986  seqdistr  13990  mulexpz  14039  leexp2r  14111  expnlbnd2  14171  expmulnbnd  14172  hashmap  14372  hashfun  14374  hashbclem  14389  hashfacen  14391  hashf1lem2  14393  hashf1  14394  ccatsymb  14520  swrdwrdsymb  14600  swrdsb0eq  14601  ccatpfx  14638  swrdswrd  14642  wrdind  14659  wrd2ind  14660  swrdccatin1  14662  swrdccatin2  14666  pfxccatin12lem2  14668  pfxccatin12  14670  swrdccat  14672  repswswrd  14721  0csh0  14730  cshwidxmod  14740  2cshw  14750  cshweqrep  14758  relexp0g  14959  relexpsucnnr  14962  relexpindlem  15000  01sqrexlem1  15179  01sqrexlem6  15184  rlim  15432  rlimclim1  15482  climsup  15607  caurcvg2  15615  caucvgb  15617  iseralt  15622  sumss  15661  fsum2dlem  15707  mptfzshft  15715  modfsummod  15731  o1fsum  15750  incexclem  15773  divrcnv  15789  flo1  15791  fprodrev  15914  fprod2dlem  15917  ruclem6  16174  moddvds  16204  dvdsaddre2b  16248  dvdsflip  16258  addmodlteqALT  16266  nn0o  16324  fldivndvdslt  16357  bitsf1ocnv  16385  bitsf1  16387  sadcaddlem  16398  bezoutlem2  16481  bezoutlem4  16483  lcmgcdlem  16547  prmind2  16626  isprm5  16648  isprm6  16655  prmdvdsncoprmbd  16668  cncongrprm  16670  hashdvds  16716  crth  16719  eulerthlem2  16723  prmdiveq  16727  hashgcdlem  16729  hashgcdeq  16731  iserodd  16777  pclem  16780  pcprendvds2  16783  pcexp  16801  pcneg  16816  pc2dvds  16821  pcmpt  16834  prmpwdvds  16846  pockthg  16848  prmreclem5  16862  4sqlem11  16897  ramub2  16956  ramubcl  16960  ram0  16964  ramub1lem2  16969  ramcl  16971  prmgaplem3  16995  prmgaplem6  16998  setscom  17121  sscpwex  17753  initoeu2  17954  setcinv  18028  funcestrcsetclem9  18085  funcsetcestrclem9  18100  fullsetcestrc  18103  1stfcl  18134  2ndfcl  18135  hofpropd  18204  isacs3lem  18479  isacs4lem  18481  acsmap2d  18492  chnflenfi  18565  subsubmgm  18649  submnd0  18702  mndpsuppss  18704  subsubm  18755  insubm  18757  frmdup1  18803  frmdup3lem  18805  sgrp2nmndlem2  18866  isgrpinv  18940  subsubg  19096  cycsubgcl  19152  conjghm  19195  qusghm  19201  gsumwrev  19312  gsmsymgrfixlem1  19373  symgfixelsi  19381  symgsssg  19413  symgfisg  19414  psgnunilem2  19441  odf1o2  19519  sylow1lem1  19544  odcau  19550  pgpfi  19551  pgpssslw  19560  fislw  19571  efgtlen  19672  efginvrel2  19673  efgrelexlemb  19696  efgredeu  19698  efgcpbllemb  19701  frgpup1  19721  lt6abl  19841  gsum2d  19918  gsum2d2lem  19919  gsum2d2  19920  telgsumfzslem  19934  dmdprdsplit2lem  19993  ablfacrp  20014  pgpfac1lem3  20025  gsummgp0  20270  irredrmul  20380  subsubrng  20513  subsubrg  20548  rngcinv  20587  ringcinv  20621  fldhmsubc  20735  islss4  20930  lspextmo  21025  lspsnat  21117  prmirredlem  21444  znf1o  21523  znidomb  21533  frgpcyg  21545  psgnghm  21552  psgndiflemB  21572  frlmlbs  21769  frlmup1  21770  lindfind  21788  islindf3  21798  lindfmm  21799  issubassa3  21838  resspsradd  21947  resspsrmul  21948  psdmul  22126  coe1tmmul2  22235  pf1ind  22316  mamulid  22402  mat1dimelbas  22432  mdetdiaglem  22559  mdetralt2  22570  mndifsplit  22597  smadiadetglem2  22633  1elcpmat  22676  pmatcollpw3lem  22744  chfacfisf  22815  chfacfisfcpmat  22816  chfacffsupp  22817  chfacfscmulfsupp  22820  chfacfscmulgsum  22821  chfacfpmmulfsupp  22824  chfacfpmmulgsum  22825  chfacfpmmulgsum2  22826  cayhamlem1  22827  cpmadugsumlemF  22837  cayleyhamilton1  22853  tgcl  22930  pptbas  22969  clsval2  23011  mretopd  23053  lmbr2  23220  cncls2  23234  nrmsep  23318  regsep2  23337  cmpsublem  23360  cmpsub  23361  tgcmp  23362  uncmp  23364  hauscmplem  23367  iunconnlem  23388  1stcrest  23414  2ndcctbss  23416  2ndcsep  23420  dis2ndc  23421  hausllycmp  23455  dislly  23458  kgentopon  23499  1stckgen  23515  kgencn3  23519  ptpjpre1  23532  ptbasin  23538  ptpjopn  23573  dfac14  23579  ptcnplem  23582  txcn  23587  txindis  23595  txdis1cn  23596  ptrescn  23600  txcmplem1  23602  txcmp  23604  txhaus  23608  txlm  23609  tx1stc  23611  txkgen  23613  xkococn  23621  qtopcn  23675  kqreglem1  23702  kqreglem2  23703  kqnrmlem1  23704  kqnrmlem2  23705  hmeoimaf1o  23731  reghmph  23754  nrmhmph  23755  txhmeo  23764  ptuncnv  23768  filconn  23844  fbasrn  23845  fmfnfmlem2  23916  flimfnfcls  23989  cnpfcfi  24001  alexsublem  24005  alexsubALTlem2  24009  alexsubALTlem3  24010  alexsubALTlem4  24011  alexsubALT  24012  ptcmplem3  24015  cnextfval  24023  tsmsxp  24116  imasdsf1olem  24334  bl2in  24361  blssps  24385  blss  24386  blssexps  24387  blssex  24388  blcld  24466  stdbdxmet  24476  met1stc  24482  prdsxmslem2  24490  metcnp3  24501  metcnpi3  24507  txmetcnp  24508  nmo0  24696  nmoid  24703  icccmplem1  24784  icccmp  24787  xrge0tsms  24796  metdseq0  24816  cnheiborlem  24926  cnheibor  24927  cnllycmp  24928  pcoval2  24989  cmetcaulem  25261  iscmet3lem1  25264  iscmet3lem2  25265  equivcau  25273  lmcau  25286  cncmet  25295  ivthlem2  25426  ivthlem3  25427  ovoliunlem2  25477  ovolscalem2  25488  uniioombl  25563  dyaddisj  25570  opnmbllem  25575  volivth  25581  ismbfd  25613  ismbf3d  25628  mbfimaopnlem  25629  mbfinf  25639  itg1addlem4  25673  mbfi1fseqlem1  25689  mbfi1fseqlem3  25691  mbfi1fseqlem4  25692  mbfi1fseqlem5  25693  mbfi1fseqlem6  25694  itg2seq  25716  itg2lea  25718  itg2split  25723  itg2cnlem1  25735  bddiblnc  25816  limciun  25868  dvmptfsum  25952  rolle  25967  c1lip1  25975  dvcnvrelem1  25995  dvcnvre  25997  dvcvx  25998  itgsubst  26029  tdeglem4  26038  mdegmullem  26056  plyco0  26170  coemullem  26228  dgreq0  26244  dgrmul  26249  dgrco  26254  elqaalem2  26301  aannenlem1  26309  aaliou3lem9  26331  ulmres  26370  ulmshftlem  26371  angneg  26786  dcubic  26829  cxploglim  26961  cxploglim2  26962  scvxcvx  26969  lgamgulmlem5  27016  lgamcvg2  27038  ftalem2  27057  basellem3  27066  basellem4  27067  sqff1o  27165  fsumdvdsdiaglem  27166  dvdsflsumcom  27171  mpodvdsmulf1o  27177  dvdsmulf1o  27179  fsumvma2  27198  logfac2  27201  logfacrlim  27208  logexprlim  27209  dchrelbasd  27223  lgsne0  27319  lgsqrlem2  27331  lgsqrmodndvds  27337  gausslemma2dlem1a  27349  lgseisenlem2  27360  lgsquadlem1  27364  lgsquadlem2  27365  lgsquadlem3  27366  lgsquad2lem2  27369  2sqlem8  27410  2sqlem11  27413  2sqreultlem  27431  2sqreunnltlem  27434  chpo1ubb  27465  vmadivsum  27466  rplogsumlem2  27469  rpvmasumlem  27471  dchrmusum2  27478  dchrvmasumlem1  27479  dchrisum0fno1  27495  dchrisum0re  27497  dchrisum0lem1  27500  dchrisum0lem2  27502  dchrisum0lem3  27503  dchrisum0  27504  mulogsumlem  27515  mulog2sumlem2  27519  vmalogdivsum2  27522  logsqvma  27526  log2sumbnd  27528  selberglem3  27531  selberg  27532  selberg2lem  27534  selberg2b  27536  selberg3lem2  27542  pntrmax  27548  pntrsumo1  27549  pntlemn  27584  pntlemp  27594  qabvle  27609  ostthlem1  27611  ostthlem2  27612  ostth2lem2  27618  ostth3  27622  ltsres  27647  nosupno  27688  nosupbnd2  27701  noinfno  27703  noinfbnd2  27716  etaslts  27806  cuteq1  27830  addsproplem2  27983  mulsval  28122  precsexlem11  28230  n0fincut  28368  zmulscld  28410  bdayfinbndlem1  28480  idmot  28627  brbtwn2  28996  colinearalglem4  29000  colinearalg  29001  ax5seglem9  29028  axpaschlem  29031  axcontlem2  29056  axcontlem7  29061  axcontlem8  29062  eengtrkg  29077  upgr1eopALT  29208  uspgredg2vlem  29314  subumgr  29379  nbgr0edglem  29447  edgnbusgreu  29458  nb3grprlem1  29471  wlkl1loop  29729  pthdivtx  29818  usgr2pth  29855  crctcshwlkn0  29912  wlklnwwlkln1  29959  wwlksnext  29984  clwwlkccatlem  30082  clwlkclwwlklem2a  30091  clwwlkinwwlk  30133  clwwlkn1loopb  30136  clwwlkf  30140  wwlksext2clwwlk  30150  wwlksubclwwlk  30151  clwwlknscsh  30155  clwwlknon1  30190  clwwlknonex2e  30203  1conngr  30287  n4cyclfrgr  30384  numclwwlk2lem1lem  30435  2clwwlk2clwwlk  30443  numclwwlk1lem2f1  30450  numclwlk1lem1  30462  numclwwlk2lem1  30469  numclwlk2lem2f  30470  numclwwlk7  30484  frgrogt3nreg  30490  grpoidinvlem1  30598  grpoidinvlem3  30600  grporcan  30612  nmlnoubi  30890  blocnilem  30898  ipblnfi  30949  htthlem  31011  ocsh  31377  shmodsi  31483  pjhthlem2  31486  5oalem2  31749  eigposi  31930  nmopub2tALT  32003  nmfnleub2  32020  nmcexi  32120  nmopcoi  32189  kbass3  32212  mdslmd1lem1  32419  mdslmd1lem2  32420  chirredlem2  32485  chirredlem4  32487  mdsymlem3  32499  mdsymlem5  32501  sumdmdii  32509  sumdmdlem  32512  sumdmdlem2  32513  foresf1o  32597  disjxpin  32681  1stpreimas  32802  resf1o  32826  nn0xmulclb  32868  wrdt2ind  33052  xrge0tsmsd  33173  gsumvsca1  33326  gsumvsca2  33327  islinds5  33466  1arithidomlem2  33635  mplvrpmmhm  33729  irngnzply1  33875  mdetpmtr1  34007  mdetpmtr2  34008  pstmxmet  34081  qqhghm  34172  qqhrhm  34173  esumpcvgval  34262  volmeas  34415  imambfm  34446  dya2iocnrect  34465  oddpwdc  34538  sseqf  34576  orvcgteel  34652  orvclteel  34657  ballotlemsf1o  34698  bnj1110  35164  bnj1118  35166  f1resveqaeq  35268  txpconn  35454  connpconn  35457  cnllysconn  35467  rellysconn  35473  cvmsss2  35496  cvmlift2lem9  35533  satf00  35596  fmlasuc  35608  mrsubfval  35730  mppsval  35794  dfon2lem6  36008  wzel  36044  ifscgr  36266  cgrxfr  36277  btwnconn1lem5  36313  btwnconn1lem6  36314  btwnconn1lem12  36320  brsegle  36330  finminlem  36540  nn0prpwlem  36544  fnessref  36579  refssfne  36580  neibastop1  36581  topjoin  36587  fnemeet2  36589  weiunse  36690  bj-prmoore  37395  bj-finsumval0  37567  topdifinffinlem  37629  lindsadd  37893  matunitlindflem2  37897  poimirlem28  37928  poimirlem32  37932  opnmbllem0  37936  mblfinlem1  37937  mblfinlem4  37940  ismblfin  37941  mbfresfi  37946  itg2addnclem  37951  itg2addnclem3  37953  itg2addnc  37954  unirep  37994  frinfm  38015  sdclem2  38022  geomcau  38039  istotbnd3  38051  sstotbnd2  38054  sstotbnd  38055  sstotbnd3  38056  totbndbnd  38069  cntotbnd  38076  ismtyres  38088  heibor1lem  38089  heiborlem1  38091  heiborlem8  38098  ismndo1  38153  isdivrngo  38230  unichnidl  38311  erimeq2  39043  cvlcvr1  39744  ishlat3N  39759  llnmlplnN  39944  islvol2aN  39997  4atlem4c  40006  4atlem4d  40007  isline2  40179  isline3  40181  linepsubclN  40356  lhpexle3lem  40416  lhpjat2  40426  cdlemd4  40606  cdleme0cq  40620  cdleme32fva  40842  cdleme32fvaw  40844  tendo0mul  41231  tendo0mulr  41232  diameetN  41461  dvhvaddcl  41500  dvhvaddcomN  41501  cdlemm10N  41523  dvadiaN  41533  djavalN  41540  dihvalcqat  41644  dihopelvalcpre  41653  djhval  41803  dihjat1lem  41833  sticksstones11  42555  sticksstones22  42567  f1o2d2  42634  remul01  42806  zaddcom  42863  zmulcom  42867  fidomncyc  42934  evlselvlem  42973  evlselv  42974  fsuppind  42977  mhpind  42981  prjspertr  42992  prjsprellsp  42998  elrfi  43080  nacsfix  43098  fzsplit1nn0  43140  eldioph2  43148  lzenom  43156  irrapxlem3  43210  pellexlem5  43219  pell1234qrne0  43239  pell1234qrmulcl  43241  pell14qrdich  43255  pell1qrge1  43256  pellqrex  43265  reglogltb  43277  reglogleb  43278  rmxypairf1o  43297  rmxycomplete  43303  monotoddzzfi  43328  congadd  43352  congsym  43354  acongrep  43366  jm2.19lem3  43377  jm2.19lem4  43378  jm2.22  43381  jm2.25  43385  expdiophlem1  43407  wepwsolem  43428  kelac1  43449  lmhmfgsplit  43472  pwslnm  43480  hbtlem6  43515  hbt  43516  mon1psubm  43585  deg1mhm  43586  omord2lim  43686  succlg  43714  onmcl  43717  ofoafo  43742  ofoacom  43747  fzunt  43840  fzuntd  43841  fzunt1d  43842  fzuntgd  43843  iunrelexp0  44087  dssmapnvod  44405  gsumws3  44581  gsumws4  44582  mulltgt0  45411  fnchoice  45418  disjrnmpt2  45576  fzisoeu  45691  fsumiunss  45964  climinf  45995  mullimc  46005  mullimcf  46012  stoweidlem14  46401  stoweidlem17  46404  stoweidlem34  46421  stoweidlem50  46437  fourierdlem42  46536  fourierdlem62  46555  fourierdlem71  46564  fourierdlem76  46569  qndenserrnbllem  46681  subsaliuncl  46745  sge0resplit  46793  3f1oss1  47464  2reu8i  47502  addmodne  47733  fundcmpsurinjpreimafv  47797  iccpartigtl  47812  prproropf1olem2  47893  prproropf1olem4  47895  paireqne  47900  prmdvdsfmtnof1lem2  47974  bgoldbtbndlem3  48196  bgoldbtbnd  48198  grimcnv  48277  gricushgr  48306  cycldlenngric  48317  grimedg  48324  grtrimap  48337  isubgr3stgrlem6  48360  isubgr3stgrlem7  48361  isubgr3stgrlem8  48362  isubgr3stgrlem9  48363  grlimfn  48368  gpgedg2iv  48456  gpg5nbgrvtx03starlem2  48458  gpg5nbgrvtx13starlem2  48461  uspgrsprf1  48536  isassintop  48599  2zlidl  48629  2zrngnmrid  48645  rngcinvALTV  48665  funcringcsetcALTV2lem9  48687  ringcinvALTV  48699  funcringcsetclem9ALTV  48710  fldhmsubcALTV  48722  gsumlsscl  48769  lincsum  48818  lindslinindsimp1  48846  lindslinindimp2lem4  48850  lincresunitlem2  48865  elfzolborelfzop1  48908  elbigo2  48941  digexp  48996  dig1  48997  nn0sumshdiglemB  49009  1arymaptf1  49031  2arymaptf1  49042  itcoval1  49052  itcoval2  49053  itcoval3  49054  itcovalsucov  49057  ackvalsuc1mpt  49067  itschlc0xyqsol  49156  brab2dd  49216  dmrnxp  49225  xpco2  49245  initopropd  49631  termopropd  49632  zeroopropd  49633  prcofpropd  49767  thincciso  49841  indthinc  49850  indthincALT  49851  oduoppcciso  49954  lanpropd  50003  ranpropd  50004