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  5116  reusv2lem4  5371  axprlem5OLD  5400  fr2nr  5631  somin1  6122  tz7.7  6378  f1oprg  6862  soisores  7319  elovmporab1w  7652  elovmporab1  7653  sorpssi  7721  onint  7782  ordsucelsuc  7814  elxp5  7917  resf1extb  7928  f1oabexg  7936  wemoiso  7970  wemoiso2  7971  el2xptp0  8033  frxp2  8141  frxp3  8148  ressuppss  8180  fprlem1  8297  tz7.48lem  8453  oalimcl  8570  oeeui  8612  nnaordex2  8649  oaabs2  8659  omabs  8661  swoer  8748  ralxpmap  8908  pw2f1olem  9088  enfixsn  9093  mapxpen  9155  mapunen  9158  php  9219  unxpdomlem2  9257  unxpdomlem3  9258  findcard3OLD  9289  isfinite2  9304  fodomfi  9320  domunfican  9331  fodomfiOLD  9340  fissuni  9367  fipreima  9368  indexfi  9370  fsuppsssupp  9391  marypha1lem  9443  marypha2  9449  supmo  9462  infmo  9507  oieu  9551  brwdom2  9585  ixpiunwdom  9602  cantnfval2  9681  cantnfle  9683  cantnflt  9684  cantnf  9705  wemapwe  9709  cnfcom  9712  frrlem15  9769  rankonidlem  9840  r1pwcl  9859  eldju2ndl  9936  eldju2ndr  9937  djuun  9938  infxpenlem  10025  infxpenc2lem1  10031  fseqenlem1  10036  dfac8clem  10044  mappwen  10124  dfac3  10133  dfac5  10141  dfac12lem3  10158  infunsdom  10225  coftr  10285  ssfin4  10322  domfin4  10323  fin23lem26  10337  fin23lem22  10339  fin23lem28  10352  fin23lem32  10356  fin23lem40  10363  isf32lem5  10369  compssiso  10386  isf34lem4  10389  isfin1-3  10398  fin1a2lem13  10424  hsmexlem2  10439  hsmexlem4  10441  zorn2lem1  10508  ttukeylem6  10526  iundom2g  10552  konigthlem  10580  pwcfsdom  10595  fpwwe2lem11  10653  fpwwe2  10655  pwfseqlem3  10672  winalim2  10708  r1wunlim  10749  inttsk  10786  inar1  10787  grur1  10832  nqereq  10947  ltexprlem7  11054  prlem936  11059  00id  11408  addlid  11416  ltord1  11761  divdiv1  11950  divdiv2  11951  conjmul  11956  ltdivmul  12115  ledivmul  12116  lt2mul2div  12118  ltdiv23  12131  lediv23  12132  lediv12a  12133  ledivp1  12142  negfi  12189  nn0nndivcl  12571  nn0ge0div  12660  peano2uz2  12679  peano5uzi  12680  eluzp1m1  12876  qbtwnre  13213  xralrple  13219  xleadd1a  13267  xmulge0  13298  xmulass  13301  xlemul1a  13302  iooshf  13441  divelunit  13509  eluzgtdifelfzo  13741  modadd1  13923  modmul1  13940  seqcl2  14036  seqfveq2  14040  seqid2  14064  seqhomo  14065  seqdistr  14069  mulexpz  14118  leexp2r  14190  expnlbnd2  14250  expmulnbnd  14251  hashmap  14451  hashfun  14453  hashbclem  14468  hashfacen  14470  hashf1lem2  14472  hashf1  14473  ccatsymb  14598  swrdwrdsymb  14678  swrdsb0eq  14679  ccatpfx  14717  swrdswrd  14721  wrdind  14738  wrd2ind  14739  swrdccatin1  14741  swrdccatin2  14745  pfxccatin12lem2  14747  pfxccatin12  14749  swrdccat  14751  repswswrd  14800  0csh0  14809  cshwidxmod  14819  2cshw  14829  cshweqrep  14837  relexp0g  15039  relexpsucnnr  15042  relexpindlem  15080  01sqrexlem1  15259  01sqrexlem6  15264  rlim  15509  rlimclim1  15559  climsup  15684  caurcvg2  15692  caucvgb  15694  iseralt  15699  sumss  15738  fsum2dlem  15784  mptfzshft  15792  modfsummod  15808  o1fsum  15827  incexclem  15850  divrcnv  15866  flo1  15868  fprodrev  15991  fprod2dlem  15994  ruclem6  16251  moddvds  16281  dvdsaddre2b  16324  dvdsflip  16334  addmodlteqALT  16342  nn0o  16400  fldivndvdslt  16433  bitsf1ocnv  16461  bitsf1  16463  sadcaddlem  16474  bezoutlem2  16557  bezoutlem4  16559  lcmgcdlem  16623  prmind2  16702  isprm5  16724  isprm6  16731  prmdvdsncoprmbd  16744  cncongrprm  16746  hashdvds  16792  crth  16795  eulerthlem2  16799  prmdiveq  16803  hashgcdlem  16805  hashgcdeq  16807  iserodd  16853  pclem  16856  pcprendvds2  16859  pcexp  16877  pcneg  16892  pc2dvds  16897  pcmpt  16910  prmpwdvds  16922  pockthg  16924  prmreclem5  16938  4sqlem11  16973  ramub2  17032  ramubcl  17036  ram0  17040  ramub1lem2  17045  ramcl  17047  prmgaplem3  17071  prmgaplem6  17074  setscom  17197  sscpwex  17826  initoeu2  18027  setcinv  18101  funcestrcsetclem9  18158  funcsetcestrclem9  18173  fullsetcestrc  18176  1stfcl  18207  2ndfcl  18208  hofpropd  18277  isacs3lem  18550  isacs4lem  18552  acsmap2d  18563  subsubmgm  18686  submnd0  18739  mndpsuppss  18741  subsubm  18792  insubm  18794  frmdup1  18840  frmdup3lem  18842  sgrp2nmndlem2  18900  isgrpinv  18974  subsubg  19130  cycsubgcl  19187  conjghm  19230  qusghm  19236  gsumwrev  19347  gsmsymgrfixlem1  19406  symgfixelsi  19414  symgsssg  19446  symgfisg  19447  psgnunilem2  19474  odf1o2  19552  sylow1lem1  19577  odcau  19583  pgpfi  19584  pgpssslw  19593  fislw  19604  efgtlen  19705  efginvrel2  19706  efgrelexlemb  19729  efgredeu  19731  efgcpbllemb  19734  frgpup1  19754  lt6abl  19874  gsum2d  19951  gsum2d2lem  19952  gsum2d2  19953  telgsumfzslem  19967  dmdprdsplit2lem  20026  ablfacrp  20047  pgpfac1lem3  20058  gsummgp0  20276  irredrmul  20385  subsubrng  20521  subsubrg  20556  rngcinv  20595  ringcinv  20629  fldhmsubc  20743  islss4  20917  lspextmo  21012  lspsnat  21104  prmirredlem  21431  znf1o  21510  znidomb  21520  frgpcyg  21532  psgnghm  21538  psgndiflemB  21558  frlmlbs  21755  frlmup1  21756  lindfind  21774  islindf3  21784  lindfmm  21785  issubassa3  21824  resspsradd  21933  resspsrmul  21934  psdmul  22102  coe1tmmul2  22211  pf1ind  22291  mamulid  22377  mat1dimelbas  22407  mdetdiaglem  22534  mdetralt2  22545  mndifsplit  22572  smadiadetglem2  22608  1elcpmat  22651  pmatcollpw3lem  22719  chfacfisf  22790  chfacfisfcpmat  22791  chfacffsupp  22792  chfacfscmulfsupp  22795  chfacfscmulgsum  22796  chfacfpmmulfsupp  22799  chfacfpmmulgsum  22800  chfacfpmmulgsum2  22801  cayhamlem1  22802  cpmadugsumlemF  22812  cayleyhamilton1  22828  tgcl  22905  pptbas  22944  clsval2  22986  mretopd  23028  lmbr2  23195  cncls2  23209  nrmsep  23293  regsep2  23312  cmpsublem  23335  cmpsub  23336  tgcmp  23337  uncmp  23339  hauscmplem  23342  iunconnlem  23363  1stcrest  23389  2ndcctbss  23391  2ndcsep  23395  dis2ndc  23396  hausllycmp  23430  dislly  23433  kgentopon  23474  1stckgen  23490  kgencn3  23494  ptpjpre1  23507  ptbasin  23513  ptpjopn  23548  dfac14  23554  ptcnplem  23557  txcn  23562  txindis  23570  txdis1cn  23571  ptrescn  23575  txcmplem1  23577  txcmp  23579  txhaus  23583  txlm  23584  tx1stc  23586  txkgen  23588  xkococn  23596  qtopcn  23650  kqreglem1  23677  kqreglem2  23678  kqnrmlem1  23679  kqnrmlem2  23680  hmeoimaf1o  23706  reghmph  23729  nrmhmph  23730  txhmeo  23739  ptuncnv  23743  filconn  23819  fbasrn  23820  fmfnfmlem2  23891  flimfnfcls  23964  cnpfcfi  23976  alexsublem  23980  alexsubALTlem2  23984  alexsubALTlem3  23985  alexsubALTlem4  23986  alexsubALT  23987  ptcmplem3  23990  cnextfval  23998  tsmsxp  24091  imasdsf1olem  24310  bl2in  24337  blssps  24361  blss  24362  blssexps  24363  blssex  24364  blcld  24442  stdbdxmet  24452  met1stc  24458  prdsxmslem2  24466  metcnp3  24477  metcnpi3  24483  txmetcnp  24484  nmo0  24672  nmoid  24679  icccmplem1  24760  icccmp  24763  xrge0tsms  24772  metdseq0  24792  cnheiborlem  24902  cnheibor  24903  cnllycmp  24904  pcoval2  24965  cmetcaulem  25238  iscmet3lem1  25241  iscmet3lem2  25242  equivcau  25250  lmcau  25263  cncmet  25272  ivthlem2  25403  ivthlem3  25404  ovoliunlem2  25454  ovolscalem2  25465  uniioombl  25540  dyaddisj  25547  opnmbllem  25552  volivth  25558  ismbfd  25590  ismbf3d  25605  mbfimaopnlem  25606  mbfinf  25616  itg1addlem4  25650  mbfi1fseqlem1  25666  mbfi1fseqlem3  25668  mbfi1fseqlem4  25669  mbfi1fseqlem5  25670  mbfi1fseqlem6  25671  itg2seq  25693  itg2lea  25695  itg2split  25700  itg2cnlem1  25712  bddiblnc  25793  limciun  25845  dvmptfsum  25929  rolle  25944  c1lip1  25952  dvcnvrelem1  25972  dvcnvre  25974  dvcvx  25975  itgsubst  26006  tdeglem4  26015  mdegmullem  26033  plyco0  26147  coemullem  26205  dgreq0  26221  dgrmul  26226  dgrco  26231  elqaalem2  26278  aannenlem1  26286  aaliou3lem9  26308  ulmres  26347  ulmshftlem  26348  angneg  26763  dcubic  26806  cxploglim  26938  cxploglim2  26939  scvxcvx  26946  lgamgulmlem5  26993  lgamcvg2  27015  ftalem2  27034  basellem3  27043  basellem4  27044  sqff1o  27142  fsumdvdsdiaglem  27143  dvdsflsumcom  27148  mpodvdsmulf1o  27154  dvdsmulf1o  27156  fsumvma2  27175  logfac2  27178  logfacrlim  27185  logexprlim  27186  dchrelbasd  27200  lgsne0  27296  lgsqrlem2  27308  lgsqrmodndvds  27314  gausslemma2dlem1a  27326  lgseisenlem2  27337  lgsquadlem1  27341  lgsquadlem2  27342  lgsquadlem3  27343  lgsquad2lem2  27346  2sqlem8  27387  2sqlem11  27390  2sqreultlem  27408  2sqreunnltlem  27411  chpo1ubb  27442  vmadivsum  27443  rplogsumlem2  27446  rpvmasumlem  27448  dchrmusum2  27455  dchrvmasumlem1  27456  dchrisum0fno1  27472  dchrisum0re  27474  dchrisum0lem1  27477  dchrisum0lem2  27479  dchrisum0lem3  27480  dchrisum0  27481  mulogsumlem  27492  mulog2sumlem2  27496  vmalogdivsum2  27499  logsqvma  27503  log2sumbnd  27505  selberglem3  27508  selberg  27509  selberg2lem  27511  selberg2b  27513  selberg3lem2  27519  pntrmax  27525  pntrsumo1  27526  pntlemn  27561  pntlemp  27571  qabvle  27586  ostthlem1  27588  ostthlem2  27589  ostth2lem2  27595  ostth3  27599  sltres  27624  nosupno  27665  nosupbnd2  27678  noinfno  27680  noinfbnd2  27693  etasslt  27775  cuteq1  27795  addsproplem2  27920  mulsval  28052  precsexlem11  28158  zmulscld  28300  idmot  28462  brbtwn2  28830  colinearalglem4  28834  colinearalg  28835  ax5seglem9  28862  axpaschlem  28865  axcontlem2  28890  axcontlem7  28895  axcontlem8  28896  eengtrkg  28911  upgr1eopALT  29042  uspgredg2vlem  29148  subumgr  29213  nbgr0edglem  29281  edgnbusgreu  29292  nb3grprlem1  29305  wlkl1loop  29564  pthdivtx  29655  usgr2pth  29692  crctcshwlkn0  29749  wlklnwwlkln1  29796  wwlksnext  29821  clwwlkccatlem  29916  clwlkclwwlklem2a  29925  clwwlkinwwlk  29967  clwwlkn1loopb  29970  clwwlkf  29974  wwlksext2clwwlk  29984  wwlksubclwwlk  29985  clwwlknscsh  29989  clwwlknon1  30024  clwwlknonex2e  30037  1conngr  30121  n4cyclfrgr  30218  numclwwlk2lem1lem  30269  2clwwlk2clwwlk  30277  numclwwlk1lem2f1  30284  numclwlk1lem1  30296  numclwwlk2lem1  30303  numclwlk2lem2f  30304  numclwwlk7  30318  frgrogt3nreg  30324  grpoidinvlem1  30431  grpoidinvlem3  30433  grporcan  30445  nmlnoubi  30723  blocnilem  30731  ipblnfi  30782  htthlem  30844  ocsh  31210  shmodsi  31316  pjhthlem2  31319  5oalem2  31582  eigposi  31763  nmopub2tALT  31836  nmfnleub2  31853  nmcexi  31953  nmopcoi  32022  kbass3  32045  mdslmd1lem1  32252  mdslmd1lem2  32253  chirredlem2  32318  chirredlem4  32320  mdsymlem3  32332  mdsymlem5  32334  sumdmdii  32342  sumdmdlem  32345  sumdmdlem2  32346  foresf1o  32431  disjxpin  32515  1stpreimas  32629  resf1o  32653  nn0xmulclb  32694  wrdt2ind  32875  xrge0tsmsd  33002  gsumvsca1  33169  gsumvsca2  33170  islinds5  33328  1arithidomlem2  33497  irngnzply1  33678  mdetpmtr1  33800  mdetpmtr2  33801  pstmxmet  33874  qqhghm  33965  qqhrhm  33966  esumpcvgval  34055  volmeas  34208  imambfm  34240  dya2iocnrect  34259  oddpwdc  34332  sseqf  34370  orvcgteel  34446  orvclteel  34451  ballotlemsf1o  34492  bnj1110  34959  bnj1118  34961  f1resveqaeq  35062  txpconn  35200  connpconn  35203  cnllysconn  35213  rellysconn  35219  cvmsss2  35242  cvmlift2lem9  35279  satf00  35342  fmlasuc  35354  mrsubfval  35476  mppsval  35540  dfon2lem6  35752  wzel  35788  ifscgr  36008  cgrxfr  36019  btwnconn1lem5  36055  btwnconn1lem6  36056  btwnconn1lem12  36062  brsegle  36072  finminlem  36282  nn0prpwlem  36286  fnessref  36321  refssfne  36322  neibastop1  36323  topjoin  36329  fnemeet2  36331  weiunse  36432  bj-prmoore  37079  bj-finsumval0  37249  topdifinffinlem  37311  lindsadd  37583  matunitlindflem2  37587  poimirlem28  37618  poimirlem32  37622  opnmbllem0  37626  mblfinlem1  37627  mblfinlem4  37630  ismblfin  37631  mbfresfi  37636  itg2addnclem  37641  itg2addnclem3  37643  itg2addnc  37644  unirep  37684  frinfm  37705  sdclem2  37712  geomcau  37729  istotbnd3  37741  sstotbnd2  37744  sstotbnd  37745  sstotbnd3  37746  totbndbnd  37759  cntotbnd  37766  ismtyres  37778  heibor1lem  37779  heiborlem1  37781  heiborlem8  37788  ismndo1  37843  isdivrngo  37920  unichnidl  38001  erimeq2  38642  cvlcvr1  39303  ishlat3N  39318  llnmlplnN  39504  islvol2aN  39557  4atlem4c  39566  4atlem4d  39567  isline2  39739  isline3  39741  linepsubclN  39916  lhpexle3lem  39976  lhpjat2  39986  cdlemd4  40166  cdleme0cq  40180  cdleme32fva  40402  cdleme32fvaw  40404  tendo0mul  40791  tendo0mulr  40792  diameetN  41021  dvhvaddcl  41060  dvhvaddcomN  41061  cdlemm10N  41083  dvadiaN  41093  djavalN  41100  dihvalcqat  41204  dihopelvalcpre  41213  djhval  41363  dihjat1lem  41393  sticksstones11  42115  sticksstones22  42127  metakunt15  42178  metakunt16  42179  f1o2d2  42231  remul01  42397  zaddcom  42442  zmulcom  42446  fidomncyc  42505  evlselvlem  42556  evlselv  42557  fsuppind  42560  mhpind  42564  prjspertr  42575  prjsprellsp  42581  elrfi  42664  nacsfix  42682  fzsplit1nn0  42724  eldioph2  42732  lzenom  42740  irrapxlem3  42794  pellexlem5  42803  pell1234qrne0  42823  pell1234qrmulcl  42825  pell14qrdich  42839  pell1qrge1  42840  pellqrex  42849  reglogltb  42861  reglogleb  42862  rmxypairf1o  42882  rmxycomplete  42888  monotoddzzfi  42913  congadd  42937  congsym  42939  acongrep  42951  jm2.19lem3  42962  jm2.19lem4  42963  jm2.22  42966  jm2.25  42970  expdiophlem1  42992  wepwsolem  43013  kelac1  43034  lmhmfgsplit  43057  pwslnm  43065  hbtlem6  43100  hbt  43101  mon1psubm  43170  deg1mhm  43171  omord2lim  43271  succlg  43299  onmcl  43302  ofoafo  43327  ofoacom  43332  fzunt  43426  fzuntd  43427  fzunt1d  43428  fzuntgd  43429  iunrelexp0  43673  dssmapnvod  43991  gsumws3  44167  gsumws4  44168  mulltgt0  44994  fnchoice  45001  disjrnmpt2  45160  fzisoeu  45277  fsumiunss  45552  climinf  45583  mullimc  45593  mullimcf  45600  stoweidlem14  45991  stoweidlem17  45994  stoweidlem34  46011  stoweidlem50  46027  fourierdlem42  46126  fourierdlem62  46145  fourierdlem71  46154  fourierdlem76  46159  qndenserrnbllem  46271  subsaliuncl  46335  sge0resplit  46383  upwrdfi  46864  3f1oss1  47052  2reu8i  47090  addmodne  47321  fundcmpsurinjpreimafv  47370  iccpartigtl  47385  prproropf1olem2  47466  prproropf1olem4  47468  paireqne  47473  prmdvdsfmtnof1lem2  47547  bgoldbtbndlem3  47769  bgoldbtbnd  47771  grimcnv  47849  gricushgr  47878  cycldlenngric  47889  grimedg  47896  grtrimap  47908  isubgr3stgrlem6  47931  isubgr3stgrlem7  47932  isubgr3stgrlem8  47933  isubgr3stgrlem9  47934  grlimfn  47939  gpg5nbgrvtx03starlem2  48019  gpg5nbgrvtx13starlem2  48022  uspgrsprf1  48070  isassintop  48133  2zlidl  48163  2zrngnmrid  48179  rngcinvALTV  48199  funcringcsetcALTV2lem9  48221  ringcinvALTV  48233  funcringcsetclem9ALTV  48244  fldhmsubcALTV  48256  gsumlsscl  48303  lincsum  48353  lindslinindsimp1  48381  lindslinindimp2lem4  48385  lincresunitlem2  48400  elfzolborelfzop1  48443  elbigo2  48480  digexp  48535  dig1  48536  nn0sumshdiglemB  48548  1arymaptf1  48570  2arymaptf1  48581  itcoval1  48591  itcoval2  48592  itcoval3  48593  itcovalsucov  48596  ackvalsuc1mpt  48606  itschlc0xyqsol  48695  brab2dd  48754  dmrnxp  48763  initopropd  49108  termopropd  49109  zeroopropd  49110  thincciso  49287  indthinc  49296  indthincALT  49297  oduoppcciso  49391