Theorem ad2antrl 740

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 401

This theorem is used by:  simprl  782  simprll  790  simprlr  791  simprl1  1237  simprl2  1238  simprl3  1239  disjxiun  5106  reusv2lem4  5372  axprlem5OLD  5402  fr2nr  5638  somin1  6133  tz7.7  6386  f1oprg  6867  soisores  7325  elovmporab1w  7657  elovmporab1  7658  sorpssi  7726  onint  7785  ordsucelsuc  7814  elxp5  7916  resf1extb  7927  f1oabexg  7934  wemoiso  7966  wemoiso2  7967  el2xptp0  8029  mpof1o2d  8117  frxp2  8136  frxp3  8143  ressuppss  8175  fprlem1  8293  tz7.48lem  8424  oalimcl  8541  oeeui  8584  nnaordex2  8621  oaabs2  8631  omabs  8633  swoer  8722  ralxpmap  8890  pw2f1olem  9065  enfixsn  9070  mapxpen  9127  mapunen  9130  php  9187  unxpdomlem2  9213  unxpdomlem3  9214  isfinite2  9254  fodomfi  9268  domunfican  9277  fissuni  9310  fipreima  9311  indexfi  9313  fsuppsssupp  9337  marypha1lem  9389  marypha2  9395  supmo  9408  infmo  9453  oieu  9497  brwdom2  9531  ixpiunwdom  9548  cantnfval2  9634  cantnfle  9636  cantnflt  9637  cantnf  9658  wemapwe  9662  cnfcom  9665  frrlem15  9725  rankonidlem  9796  r1pwcl  9815  eldju2ndl  9915  eldju2ndr  9916  djuun  9917  infxpenlem  10002  infxpenc2lem1  10008  fseqenlem1  10013  dfac8clem  10021  mappwen  10101  dfac3  10110  dfac5  10117  dfac12lem3  10134  infunsdom  10201  coftr  10261  ssfin4  10298  domfin4  10299  fin23lem26  10313  fin23lem22  10315  fin23lem28  10328  fin23lem32  10332  fin23lem40  10339  isf32lem5  10345  compssiso  10362  isf34lem4  10365  isfin1-3  10374  fin1a2lem13  10400  hsmexlem2  10415  hsmexlem4  10417  zorn2lem1  10484  ttukeylem6  10502  iundom2g  10528  konigthlem  10557  pwcfsdom  10572  fpwwe2lem11  10630  fpwwe2  10632  pwfseqlem3  10649  winalim2  10685  r1wunlim  10726  inttsk  10763  inar1  10764  grur1  10809  nqereq  10924  ltexprlem7  11031  prlem936  11036  00id  11389  addlid  11397  ltord1  11744  divdiv1  11930  divdiv2  11931  conjmul  11936  ltdivmul  12094  ledivmul  12095  lt2mul2div  12097  ltdiv23  12110  lediv23  12111  lediv12a  12112  ledivp1  12121  negfi  12168  nn0nndivcl  12580  nn0ge0div  12669  peano2uz2  12688  peano5uzi  12689  eluzp1m1  12892  qbtwnre  13229  xralrple  13235  xleadd1a  13283  xmulge0  13314  xmulass  13317  xlemul1a  13318  iooshf  13457  divelunit  13525  eluzgtdifelfzo  13761  modadd1  13946  modmul1  13965  seqcl2  14061  seqfveq2  14065  seqid2  14089  seqhomo  14090  seqdistr  14094  mulexpz  14143  leexp2r  14215  expnlbnd2  14275  expmulnbnd  14276  hashmap  14477  hashfun  14479  hashbclem  14494  hashfacen  14496  hashf1lem2  14498  hashf1  14499  ccatsymb  14625  swrdwrdsymb  14705  swrdsb0eq  14706  ccatpfx  14743  swrdswrd  14747  wrdind  14764  wrd2ind  14765  swrdccatin1  14767  swrdccatin2  14771  pfxccatin12lem2  14773  pfxccatin12  14775  swrdccat  14777  repswswrd  14826  0csh0  14835  cshwidxmod  14845  2cshw  14855  cshweqrep  14863  relexp0g  15064  relexpsucnnr  15067  relexpindlem  15105  01sqrexlem1  15298  01sqrexlem6  15303  rlim  15551  rlimclim1  15601  climsup  15726  caurcvg2  15734  caucvgb  15736  iseralt  15741  sumss  15780  fsum2dlem  15826  mptfzshft  15834  modfsummod  15851  o1fsum  15870  incexclem  15895  divrcnv  15911  flo1  15913  fprodrev  16036  fprod2dlem  16039  ruclem6  16295  moddvds  16325  dvdsaddre2b  16369  dvdsflip  16379  addmodlteqALT  16387  nn0o  16445  fldivndvdslt  16478  bitsf1ocnv  16506  bitsf1  16508  sadcaddlem  16519  bezoutlem2  16602  bezoutlem4  16604  lcmgcdlem  16668  prmind2  16747  isprm5  16770  isprm6  16777  prmdvdsncoprmbd  16790  cncongrprm  16792  hashdvds  16838  crth  16841  eulerthlem2  16845  prmdiveq  16849  hashgcdlem  16851  hashgcdeq  16853  iserodd  16899  pclem  16902  pcprendvds2  16905  pcexp  16923  pcneg  16938  pc2dvds  16943  pcmpt  16956  prmpwdvds  16968  pockthg  16970  prmreclem5  16984  4sqlem11  17019  ramub2  17078  ramubcl  17082  ram0  17086  ramub1lem2  17091  ramcl  17093  prmgaplem3  17117  prmgaplem6  17120  setscom  17244  sscpwex  17876  initoeu2  18077  setcinv  18151  funcestrcsetclem9  18208  funcsetcestrclem9  18223  fullsetcestrc  18226  1stfcl  18257  2ndfcl  18258  hofpropd  18327  isacs3lem  18602  isacs4lem  18604  acsmap2d  18615  chnflenfi  18688  subsubmgm  18772  submnd0  18825  mndpsuppss  18827  subsubm  18879  insubm  18881  frmdup1  18927  frmdup3lem  18929  sgrp2nmndlem2  18990  isgrpinv  19064  subsubg  19220  cycsubgcl  19281  conjghm  19323  qusghm  19329  gsumwrev  19440  gsmsymgrfixlem1  19501  symgfixelsi  19509  symgsssg  19541  symgfisg  19542  psgnunilem2  19569  odf1o2  19647  sylow1lem1  19672  odcau  19678  pgpfi  19679  pgpssslw  19688  fislw  19699  efgtlen  19800  efginvrel2  19801  efgrelexlemb  19824  efgredeu  19826  efgcpbllemb  19829  frgpup1  19849  lt6abl  19969  gsum2d  20046  gsum2d2lem  20047  gsum2d2  20048  telgsumfzslem  20062  dmdprdsplit2lem  20121  ablfacrp  20142  pgpfac1lem3  20153  gsummgp0  20404  irredrmul  20514  subsubrng  20671  subsubrg  20706  rngcinv  20745  ringcinv  20779  fldhmsubc  20897  islss4  21092  lspextmo  21186  lspsnat  21278  prmirredlem  21631  znf1o  21710  znidomb  21720  frgpcyg  21732  psgnghm  21739  psgndiflemB  21759  frlmlbs  21956  frlmup1  21957  lindfind  21975  islindf3  21985  lindfmm  21986  issubassa3  22025  resspsradd  22133  resspsrmul  22134  psdmul  22338  coe1tmmul2  22446  pf1ind  22524  mamulid  22607  mat1dimelbas  22637  mdetdiaglem  22764  mdetralt2  22775  mndifsplit  22802  smadiadetglem2  22838  1elcpmat  22881  pmatcollpw3lem  22949  chfacfisf  23020  chfacfisfcpmat  23021  chfacffsupp  23022  chfacfscmulfsupp  23025  chfacfscmulgsum  23026  chfacfpmmulfsupp  23029  chfacfpmmulgsum  23030  chfacfpmmulgsum2  23031  cayhamlem1  23032  cpmadugsumlemF  23042  cayleyhamilton1  23058  tgcl  23135  pptbas  23174  clsval2  23216  mretopd  23258  lmbr2  23425  cncls2  23439  nrmsep  23523  regsep2  23542  cmpsublem  23565  cmpsub  23566  tgcmp  23567  uncmp  23569  hauscmplem  23572  iunconnlem  23593  1stcrest  23619  2ndcctbss  23621  2ndcsep  23625  dis2ndc  23626  hausllycmp  23660  dislly  23663  kgentopon  23704  1stckgen  23720  kgencn3  23724  ptpjpre1  23737  ptbasin  23743  ptpjopn  23778  dfac14  23784  ptcnplem  23787  txcn  23792  txindis  23800  txdis1cn  23801  ptrescn  23805  txcmplem1  23807  txcmp  23809  txhaus  23813  txlm  23814  tx1stc  23816  txkgen  23818  xkococn  23826  qtopcn  23880  kqreglem1  23907  kqreglem2  23908  kqnrmlem1  23909  kqnrmlem2  23910  hmeoimaf1o  23936  reghmph  23959  nrmhmph  23960  txhmeo  23969  ptuncnv  23973  filconn  24049  fbasrn  24050  fmfnfmlem2  24121  flimfnfcls  24194  cnpfcfi  24206  alexsublem  24210  alexsubALTlem2  24214  alexsubALTlem3  24215  alexsubALTlem4  24216  alexsubALT  24217  ptcmplem3  24220  cnextfval  24228  tsmsxp  24321  imasdsf1olem  24539  bl2in  24566  blssps  24590  blss  24591  blssexps  24592  blssex  24593  blcld  24671  stdbdxmet  24681  met1stc  24687  prdsxmslem2  24695  metcnp3  24706  metcnpi3  24712  txmetcnp  24713  nmo0  24901  nmoid  24908  icccmplem1  24989  icccmp  24992  xrge0tsms  25001  metdseq0  25021  cnheiborlem  25122  cnheibor  25123  cnllycmp  25124  pcoval2  25184  cmetcaulem  25456  iscmet3lem1  25459  iscmet3lem2  25460  equivcau  25468  lmcau  25481  cncmet  25490  ivthlem2  25620  ivthlem3  25621  ovoliunlem2  25671  ovolscalem2  25682  uniioombl  25757  dyaddisj  25764  opnmbllem  25769  volivth  25775  ismbfd  25807  ismbf3d  25822  mbfimaopnlem  25823  mbfinf  25833  itg1addlem4  25867  mbfi1fseqlem1  25883  mbfi1fseqlem3  25885  mbfi1fseqlem4  25886  mbfi1fseqlem5  25887  mbfi1fseqlem6  25888  itg2seq  25910  itg2lea  25912  itg2split  25917  itg2cnlem1  25929  bddiblnc  26010  limciun  26062  dvmptfsum  26143  rolle  26158  c1lip1  26165  dvcnvrelem1  26185  dvcnvre  26187  dvcvx  26188  itgsubst  26217  tdeglem4  26226  mdegmullem  26244  plyco0  26358  coemullem  26416  dgreq0  26431  dgrmul  26436  dgrco  26441  elqaalem2  26490  aannenlem1  26500  aaliou3lem9  26522  ulmres  26560  ulmshftlem  26561  angneg  26977  dcubic  27020  cxploglim  27151  cxploglim2  27152  scvxcvx  27159  lgamgulmlem5  27206  lgamcvg2  27228  ftalem2  27247  basellem3  27256  basellem4  27257  sqff1o  27355  fsumdvdsdiaglem  27356  dvdsflsumcom  27361  mpodvdsmulf1o  27367  dvdsmulf1o  27369  fsumvma2  27387  logfac2  27390  logfacrlim  27397  logexprlim  27398  dchrelbasd  27412  lgsne0  27508  lgsqrlem2  27520  lgsqrmodndvds  27526  gausslemma2dlem1a  27538  lgseisenlem2  27549  lgsquadlem1  27553  lgsquadlem2  27554  lgsquadlem3  27555  lgsquad2lem2  27558  2sqlem8  27599  2sqlem11  27602  2sqreultlem  27620  2sqreunnltlem  27623  chpo1ubb  27654  vmadivsum  27655  rplogsumlem2  27658  rpvmasumlem  27660  dchrmusum2  27667  dchrvmasumlem1  27668  dchrisum0fno1  27684  dchrisum0re  27686  dchrisum0lem1  27689  dchrisum0lem2  27691  dchrisum0lem3  27692  dchrisum0  27693  mulogsumlem  27704  mulog2sumlem2  27708  vmalogdivsum2  27711  logsqvma  27715  log2sumbnd  27717  selberglem3  27720  selberg  27721  selberg2lem  27723  selberg2b  27725  selberg3lem2  27731  pntrmax  27737  pntrsumo1  27738  pntlemn  27773  pntlemp  27783  qabvle  27798  ostthlem1  27800  ostthlem2  27801  ostth2lem2  27807  ostth3  27811  ltsres  27835  nosupno  27876  nosupbnd2  27889  noinfno  27891  noinfbnd2  27904  etaslts  27995  cuteq1  28019  addsproplem2  28172  mulsval  28311  precsexlem11  28419  n0fincut  28557  zmulscld  28599  bdayfinbndlem1  28669  idmot  28815  plngval  29068  brbtwn2  29264  colinearalglem4  29268  colinearalg  29269  ax5seglem9  29296  axpaschlem  29299  axcontlem2  29324  axcontlem7  29329  axcontlem8  29330  eengtrkg  29345  upgr1eopALT  29476  uspgredg2vlem  29582  subumgr  29647  nbgr0edglem  29715  edgnbusgreu  29726  nb3grprlem1  29739  wlkl1loop  29996  pthdivtx  30085  usgr2pth  30122  crctcshwlkn0  30179  wlklnwwlkln1  30226  wwlksnext  30251  clwwlkccatlem  30349  clwlkclwwlklem2a  30358  clwwlkinwwlk  30400  clwwlkn1loopb  30403  clwwlkf  30407  wwlksext2clwwlk  30417  wwlksubclwwlk  30418  clwwlknscsh  30422  clwwlknon1  30457  clwwlknonex2e  30470  1conngr  30554  n4cyclfrgr  30651  numclwwlk2lem1lem  30702  2clwwlk2clwwlk  30710  numclwwlk1lem2f1  30717  numclwlk1lem1  30729  numclwwlk2lem1  30736  numclwlk2lem2f  30737  numclwwlk7  30751  frgrogt3nreg  30757  grpoidinvlem1  30865  grpoidinvlem3  30867  grporcan  30879  nmlnoubi  31157  blocnilem  31165  ipblnfi  31216  htthlem  31278  ocsh  31644  shmodsi  31750  pjhthlem2  31753  5oalem2  32016  eigposi  32197  nmopub2tALT  32270  nmfnleub2  32287  nmcexi  32387  nmopcoi  32456  kbass3  32479  mdslmd1lem1  32686  mdslmd1lem2  32687  chirredlem2  32752  chirredlem4  32754  mdsymlem3  32766  mdsymlem5  32768  sumdmdii  32776  sumdmdlem  32779  sumdmdlem2  32780  foresf1o  32859  disjxpin  32942  1stpreimas  33060  resf1o  33084  nn0xmulclb  33125  wrdt2ind  33282  xrge0tsmsd  33402  gsumvsca1  33555  gsumvsca2  33556  islinds5  33691  1arithidomlem2  33835  mplvrpmmhm  33945  irngnzply1  34090  mdetpmtr1  34222  mdetpmtr2  34223  pstmxmet  34296  qqhghm  34387  qqhrhm  34388  esumpcvgval  34477  volmeas  34630  imambfm  34661  dya2iocnrect  34680  oddpwdc  34753  sseqf  34791  orvcgteel  34867  orvclteel  34872  ballotlemsf1o  34913  bnj1110  35379  bnj1118  35381  f1resveqaeq  35482  txpconn  35732  connpconn  35735  cnllysconn  35745  rellysconn  35751  cvmsss2  35774  cvmlift2lem9  35811  satf00  35874  fmlasuc  35886  mrsubfval  36008  mppsval  36072  dfon2lem6  36286  wzel  36322  ifscgr  36544  cgrxfr  36555  btwnconn1lem5  36591  btwnconn1lem6  36592  btwnconn1lem12  36598  brsegle  36608  finminlem  36857  nn0prpwlem  36861  fnessref  36896  refssfne  36897  neibastop1  36898  topjoin  36904  fnemeet2  36906  weiunse  37007  mh-inf3f1  37080  bj-prmoore  37785  bj-finsumval0  37957  topdifinffinlem  38021  lindsadd  38292  matunitlindflem2  38296  poimirlem28  38327  poimirlem32  38331  opnmbllem0  38335  mblfinlem1  38336  mblfinlem4  38339  ismblfin  38340  mbfresfi  38345  itg2addnclem  38350  itg2addnclem3  38352  itg2addnc  38353  unirep  38393  frinfm  38414  sdclem2  38421  geomcau  38438  istotbnd3  38450  sstotbnd2  38453  sstotbnd  38454  sstotbnd3  38455  totbndbnd  38468  cntotbnd  38475  ismtyres  38487  heibor1lem  38488  heiborlem1  38490  heiborlem8  38497  ismndo1  38552  isdivrngo  38629  unichnidl  38710  erimeq2  39440  cvlcvr1  40141  ishlat3N  40156  llnmlplnN  40341  islvol2aN  40394  4atlem4c  40403  4atlem4d  40404  isline2  40576  isline3  40578  linepsubclN  40753  lhpexle3lem  40813  lhpjat2  40823  cdlemd4  41003  cdleme0cq  41017  cdleme32fva  41239  cdleme32fvaw  41241  tendo0mul  41628  tendo0mulr  41629  diameetN  41858  dvhvaddcl  41897  dvhvaddcomN  41898  cdlemm10N  41920  dvadiaN  41930  djavalN  41937  dihvalcqat  42041  dihopelvalcpre  42050  djhval  42200  dihjat1lem  42230  sticksstones11  42951  sticksstones22  42963  remul01  43196  zaddcom  43266  zmulcom  43270  fidomncyc  43331  evlselvlem  43348  evlselv  43349  fsuppind  43350  mhpind  43354  prjspertr  43365  prjsprellsp  43371  elrfi  43453  nacsfix  43471  fzsplit1nn0  43513  eldioph2  43521  lzenom  43529  irrapxlem3  43579  pellexlem5  43588  pell1234qrne0  43608  pell1234qrmulcl  43610  pell14qrdich  43624  pell1qrge1  43625  pellqrex  43634  reglogltb  43646  reglogleb  43647  rmxypairf1o  43666  rmxycomplete  43672  monotoddzzfi  43697  congadd  43721  congsym  43723  acongrep  43735  jm2.19lem3  43746  jm2.19lem4  43747  jm2.22  43750  jm2.25  43754  expdiophlem1  43776  wepwsolem  43797  kelac1  43818  lmhmfgsplit  43841  pwslnm  43849  hbtlem6  43884  hbt  43885  mon1psubm  43954  deg1mhm  43955  omord2lim  44055  succlg  44083  onmcl  44086  ofoafo  44111  ofoacom  44116  fzunt  44209  fzuntd  44210  fzunt1d  44211  fzuntgd  44212  iunrelexp0  44456  dssmapnvod  44774  gsumws3  44950  gsumws4  44951  mulltgt0  45770  fnchoice  45777  disjrnmpt2  45934  fzisoeu  46047  fsumiunss  46319  climinf  46350  mullimc  46360  mullimcf  46367  stoweidlem14  46756  stoweidlem17  46759  stoweidlem34  46776  stoweidlem50  46792  fourierdlem42  46891  fourierdlem62  46910  fourierdlem71  46919  fourierdlem76  46924  qndenserrnbllem  47036  subsaliuncl  47100  sge0resplit  47148  3f1oss1  47840  2reu8i  47878  addmodne  48115  fundcmpsurinjpreimafv  48185  iccpartigtl  48200  prproropf1olem2  48281  prproropf1olem4  48283  paireqne  48288  prmdvdsfmtnof1lem2  48365  nprmdvdsfacm1  48404  bgoldbtbndlem3  48600  bgoldbtbnd  48602  grimcnv  48681  gricushgr  48710  cycldlenngric  48721  grimedg  48728  grtrimap  48741  isubgr3stgrlem6  48764  isubgr3stgrlem7  48765  isubgr3stgrlem8  48766  isubgr3stgrlem9  48767  grlimfn  48772  gpgedg2iv  48860  gpg5nbgrvtx03starlem2  48862  gpg5nbgrvtx13starlem2  48865  uspgrsprf1  48940  isassintop  49003  2zlidl  49033  2zrngnmrid  49049  rngcinvALTV  49069  funcringcsetcALTV2lem9  49091  ringcinvALTV  49103  funcringcsetclem9ALTV  49114  fldhmsubcALTV  49126  gsumlsscl  49188  lincsum  49237  lindslinindsimp1  49265  lindslinindimp2lem4  49269  lincresunitlem2  49284  elfzolborelfzop1  49327  elbigo2  49360  digexp  49415  dig1  49416  nn0sumshdiglemB  49428  1arymaptf1  49450  2arymaptf1  49461  itcoval1  49471  itcoval2  49472  itcoval3  49473  itcovalsucov  49476  ackvalsuc1mpt  49486  itschlc0xyqsol  49575  brab2dd  49634  dmrnxp  49643  xpco2  49663  initopropd  50049  termopropd  50050  zeroopropd  50051  prcofpropd  50185  thincciso  50259  indthinc  50268  indthincALT  50269  oduoppcciso  50372  lanpropd  50421  ranpropd  50422