Theorem adantrr 718

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)

Hypothesis

Ref	Expression
adant2.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
adantrr	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃)) → 𝜒)

Proof of Theorem adantrr

Step	Hyp	Ref	Expression
1		simpl 482	. 2 ⊢ ((𝜓 ∧ 𝜃) → 𝜓)
2		adant2.1	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3	1, 2	sylan2 594	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:  ad2antrl  729  ad2ant2r  748  ad2ant2lr  749  cases2ALT  1049  consensus  1053  3adant3  1133  3ad2antr1  1190  reusv2lem3  5335  axprlem4OLD  5365  otsndisj  5465  otiunsndisj  5466  po2nr  5544  sotric  5560  sotrieq  5561  tz7.7  6341  fmptsnd  7115  fvtp1g  7144  f1cofveqaeqALT  7204  fsnex  7229  isocnv  7276  isores2  7279  isomin  7283  isoini  7284  f1oiso2  7298  ovmpodf  7514  offval  7631  ordsucun  7767  xp1st  7965  cnvf1olem  8051  fnse  8074  sexp2  8087  mpoxopoveq  8160  frrlem3  8229  frrlem13  8239  oalim  8458  omlim  8459  oaass  8487  omordi  8492  omwordri  8498  odi  8505  oen0  8513  oewordri  8519  nnawordi  8548  nnmordi  8558  omabs  8578  coflton  8598  nadd4  8625  erinxp  8729  dom2lem  8930  domssl  8936  mapen  9070  ssenen  9080  ssfiALT  9099  domfi  9114  php  9132  domunfican  9223  mapfien  9312  ordtypelem6  9429  ordtypelem7  9430  card2inf  9461  inf3lem6  9543  cantnfle  9581  cantnflem1b  9596  cantnflem1  9599  wemapwe  9607  ttrclselem2  9636  rankxplim3  9794  fseqenlem2  9936  dfac5lem4  10037  dfac5lem4OLD  10039  dfac2b  10042  cfsuc  10168  cfflb  10170  cofsmo  10180  infpssrlem4  10217  fin4en1  10220  ssfin4  10221  fin23lem26  10236  fin23lem22  10238  fin23lem27  10239  isf34lem4  10288  isf34lem5  10289  fin1a2lem12  10322  axdc3lem2  10362  axdc4lem  10366  ttukeylem6  10425  iundom2g  10451  pwcfsdom  10495  gchen2  10538  gchor  10539  fpwwe2lem6  10548  fpwwe2lem8  10550  fpwwe2lem10  10552  fpwwe2lem11  10553  fpwwe2  10555  pwfseqlem4  10574  gchina  10611  ltexprlem6  10953  prlem936  10959  mul4  11303  2addsub  11396  muladd  11571  ltleadd  11622  leord1  11666  eqord1  11667  ltord2  11668  leord2  11669  eqord2  11670  divmul3  11803  divcan7  11853  divadddiv  11859  lemul2a  11999  lemul12b  12001  ltmuldiv2  12019  ltdivmul  12020  ledivmul  12021  ltdivmul2  12022  lt2mul2div  12023  ledivmul2  12024  lemuldiv2  12026  lt2msq  12030  ltdiv23  12036  lediv23  12037  fimaxre  12089  supadd  12113  supmullem1  12115  cju  12144  zextlt  12592  suprzcl  12598  zmax  12884  xrlttr  13080  xrre3  13112  qbtwnre  13140  xrsupsslem  13248  xrinfmsslem  13249  supxrunb1  13260  supxrunb2  13261  ixxdisj  13302  iooshf  13368  icodisj  13418  iccf1o  13438  modid  13844  modadd1  13856  modmul1  13875  seqf1o  13994  expsub  14061  sqlecan  14160  bcval5  14269  hashmap  14386  hashfacen  14405  seqcoll  14415  swrdswrdlem  14655  swrdccatin2  14680  cshwidxmod  14754  2cshwcshw  14776  cshwcshid  14778  resqreu  15203  lenegsq  15272  limsupbnd2  15434  icco1  15491  rlimresb  15516  rlimsqzlem  15600  rlimsqz  15601  rlimsqz2  15602  caucvgrlem  15624  fsum0diag2  15734  o1fsum  15765  ruclem8  16193  dvdsmulcr  16243  ndvdsadd  16368  bitsshft  16433  lcmdvds  16566  hashdvds  16734  eulerthlem2  16741  phisum  16750  pcqmul  16813  pcmpt  16852  prmreclem3  16878  4sqlem11  16915  0ram  16980  ramub1  16988  invfun  17720  initoeu2lem2  17971  coaval  18024  catcisolem  18066  funcestrcsetclem8  18102  fullestrcsetc  18106  embedsetcestrclem  18112  funcsetcestrclem8  18117  fullsetcestrc  18121  prfcl  18158  prf1st  18159  prf2nd  18160  1st2ndprf  18161  curfuncf  18193  isposd  18277  lubun  18470  isacs3lem  18497  pslem  18527  psss  18535  chnccat  18581  chnpof1  18585  pwsdiagmhm  18788  grpinvid1  18956  grpinvid2  18957  grplcan  18965  grpnpncan0  19001  dfgrp3lem  19003  dfgrp3  19004  grplactcnv  19008  0nsg  19133  eqger  19142  eqg0subg  19160  qus0subgadd  19163  resghm  19196  conjghm  19213  subgga  19264  gaorber  19272  gastacl  19273  orbsta  19277  symgextf1lem  19384  psgnunilem2  19459  odid  19502  odmulg  19520  gexid  19545  odcau  19568  lsmssv  19607  lsmcom2  19619  pj1ghm  19667  frgpuptf  19734  frgpup1  19739  ghmplusg  19810  cyggex2  19861  gsumval3eu  19868  gsumval3  19871  ablfac1eu  20039  pgpfac1lem5  20045  ablsimpgfind  20076  ringurd  20155  srhmsubc  20646  isdomn4  20682  isdrngd  20731  isdrngdOLD  20733  issrngd  20821  lmhmf1o  21031  lmhmima  21032  lmhmpreima  21033  lspextmo  21041  pwssplit2  21045  pwssplit3  21046  lspdisj  21113  islbs3  21143  lbsextlem4  21149  drngnidl  21231  rngqiprngghmlem2  21276  rngqiprnglinlem1  21279  rngqiprngghm  21287  lidldvgen  21322  cnsubrg  21415  znunit  21551  cygznlem3  21557  dsmmsubg  21731  dsmmlss  21732  frlmsslsp  21784  frlmup1  21786  lindfrn  21809  f1lindf  21810  issubassa2  21880  psrbagconf1o  21917  psrgrp  21944  evlslem2  22066  mhplss  22130  psdmul  22141  psdmvr  22144  ply1sclf1  22263  mamuass  22376  dmatmul  22471  dmatsubcl  22472  dmatmulcl  22474  dmatcrng  22476  scmataddcl  22490  scmatsubcl  22491  scmatcrng  22495  mdetunilem2  22587  pm2mpf1  22773  pm2mpghm  22790  eltg2  22932  ntrss  23029  opncldf1  23058  ssnei2  23090  neindisj  23091  restopnb  23149  restntr  23156  tgcmp  23375  hauscmplem  23380  2ndc1stc  23425  2ndcdisj  23430  2ndcomap  23432  restlly  23457  lly1stc  23470  isref  23483  islocfin  23491  comppfsc  23506  txcls  23578  txdis1cn  23609  pthaus  23612  txlm  23622  qtoptop2  23673  qtopomap  23692  kqt0lem  23710  pt1hmeo  23780  ptuncnv  23781  xkocnv  23788  fbasfip  23842  fgabs  23853  fbasrn  23858  elfm2  23922  fmfnfmlem2  23929  fmfnfmlem4  23931  ptcmplem3  24028  ptcmplem4  24029  tsmsres  24118  tsmsxplem1  24127  utoptop  24208  elbl2ps  24363  elbl2  24364  blin  24395  xmeter  24407  xmetresbl  24411  stdbdxmet  24489  metrest  24498  metustexhalf  24530  dscmet  24546  nrmmetd  24548  tngngp2  24626  nmoi2  24704  icccmplem2  24798  reconnlem2  24802  metdstri  24826  metdsle  24827  metdsre  24828  metnrmlem3  24836  fsumcn  24846  icccvx  24926  bndth  24934  evth  24935  reparphti  24973  pi1blem  25015  tcphcph  25213  iscfil2  25242  cfilfcls  25250  iscau4  25255  iscauf  25256  caucfil  25259  cncmet  25298  minveclem7  25411  ovoliunlem1  25478  ovolicc2lem2  25494  ovolicc2lem3  25495  ovolicc2lem4  25496  ovolicc2lem5  25497  ovolicc2  25498  voliunlem3  25528  voliun  25530  ioombl  25541  volivth  25583  ismbfd  25615  ismbf3d  25630  itg1addlem1  25668  i1fadd  25671  itg1addlem4  25675  itg2split  25725  itg2monolem1  25726  itg2gt0  25736  ibllem  25740  itgvallem3  25762  iblposlem  25768  bddiblnc  25818  dvmptfsum  25951  rolle  25966  dvlip  25970  c1liplem1  25973  lhop1  25991  lhop2  25992  dvcvx  25997  dvfsumge  26000  dvfsumrlimge0  26009  dvfsumrlim  26010  dvfsum2  26013  mdegaddle  26051  mdegvscale  26052  mdegmullem  26055  ply1divex  26114  coeeulem  26201  plyco  26218  dgrlt  26243  vieta1  26291  ulmss  26377  ulmdvlem3  26382  iblulm  26387  tanord  26518  eff1olem  26528  logdivlt  26601  logccv  26643  lawcos  26797  xrlimcnp  26949  cxp2limlem  26957  cxp2lim  26958  cxploglim2  26960  divsqrtsumo1  26965  lgambdd  27018  sqff1o  27163  dvdsppwf1o  27167  dvdsflf1o  27168  musum  27172  muinv  27174  fsumdvdsmul  27176  fsumdvdsmulOLD  27178  sgmmul  27183  fsumvma  27195  logfac2  27199  chpchtsum  27201  logfacrlim  27206  logexprlim  27207  dchrelbas3  27220  dchrmulcl  27231  bposlem1  27266  lgsdchr  27337  lgsquadlem1  27362  lgsquadlem2  27363  lgsquad2lem2  27367  chebbnd1lem1  27451  chpchtlim  27461  rplogsumlem2  27467  dchrmusum2  27476  dchrvmasumlem1  27477  dchrvmasum2lem  27478  dchrvmasumlem2  27480  dchrvmasumlem3  27481  dchrvmasumiflem2  27484  dchrisum0flb  27492  dchrisum0fno1  27493  rpvmasum2  27494  dchrisum0re  27495  dchrisum0lem1  27498  dchrisum0lem2a  27499  dchrisum0lem2  27500  dchrisum0lem3  27501  rplogsum  27509  mulogsum  27514  mulog2sumlem2  27517  vmalogdivsum2  27520  2vmadivsumlem  27522  selberglem2  27528  selberg3lem1  27539  selberg4lem1  27542  selberg4  27543  pntrsumo1  27547  selberg34r  27553  pntrlog2bndlem1  27559  pntrlog2bndlem2  27560  pntrlog2bndlem3  27561  pntrlog2bndlem4  27562  pntrlog2bndlem5  27563  pntrlog2bndlem6  27565  pntibndlem3  27574  pntlemp  27592  ostthlem1  27609  ostth3  27620  ltsres  27645  noresle  27680  nosupno  27686  nosupbday  27688  noinfno  27701  bday1  27825  cutlt  27943  addsproplem2  27981  negsproplem2  28040  mulsuniflem  28160  mulsunif2lem  28180  precsexlem9  28226  precsexlem10  28227  precsexlem11  28228  om2noseqlt  28310  om2noseqlt2  28311  om2noseqf1o  28312  om2noseqrdg  28315  noseqrdgfn  28317  bdaypw2n0bndlem  28474  bdayfinbndlem1  28478  recut  28505  elreno2  28506  renegscl  28509  ercgrg  28604  oppperpex  28840  axlowdimlem15  29044  axlowdimlem16  29045  axcontlem10  29061  cusgrfilem1  29544  upgriswlk  29729  crctcshwlkn0  29909  wwlksnext  29981  wwlksnextwrd  29985  clwlkclwwlklem2a  30088  wwlksext2clwwlk  30147  grpoidinv  30599  grporcan  30609  grpoinvid1  30619  grpoinvid2  30620  grpolcan  30621  ablo4  30641  nvabs  30763  minvecolem7  30974  htthlem  31008  hvadd4  31127  hvaddsub4  31169  shscli  31408  pjspansn  31668  fh1  31709  fh2  31710  cm2j  31711  chscllem2  31729  spansncvi  31743  5oalem2  31746  5oalem5  31749  5oalem6  31750  3oalem2  31754  hoadd4  31875  cnvunop  32009  bralnfn  32039  eighmorth  32055  hmops  32111  hmopm  32112  adjlnop  32177  adjmul  32183  adjadd  32184  nmopcoi  32186  kbass5  32211  kbass6  32212  hstle  32321  stlesi  32332  mdsl0  32401  mdexchi  32426  atom1d  32444  superpos  32445  cvexchlem  32459  atomli  32473  atcvatlem  32476  chirredlem2  32482  chirredlem3  32483  atcvat4i  32488  mdsymlem1  32494  mdsymlem3  32496  mdsymlem5  32498  mdsymlem6  32499  sumdmdlem  32509  sumdmdlem2  32510  cdj1i  32524  opeldifid  32689  isoun  32795  1stpreimas  32799  f1od2  32812  indf1ofs  32946  ccatf1  33029  archirngz  33270  archiabllem1  33274  archiabllem2c  33276  qusxpid  33443  esum2d  34258  cntmeas  34391  ddemeas  34401  carsgclctunlem1  34482  itgeq12dv  34491  eulerpartlemgc  34527  eulerpartlemb  34533  eulerpartlemgs2  34545  ballotlemfc0  34658  ballotlemfcc  34659  reprss  34782  reprpmtf1o  34791  hgt750lemb  34821  bnj607  35079  fissorduni  35254  derangenlem  35374  subfacp1lem3  35385  subfacp1lem5  35387  cvmliftmolem2  35485  cvmliftlem6  35493  cvmlift2lem5  35510  cvmlift2lem7  35512  cvmlift2lem9  35514  mppspstlem  35774  dfon2lem6  35989  colinbtwnle  36321  finminlem  36521  nn0prpwlem  36525  isfne  36542  neibastop1  36562  neibastop2lem  36563  neibastop3  36565  tailfb  36580  onsuct0  36644  nndivsub  36660  knoppcnlem6  36771  knoppndvlem9  36793  knoppndvlem18  36802  knoppndvlem21  36805  bj-prmoore  37440  bj-finsumval0  37612  rdgeqoa  37697  pibt2  37744  lindsadd  37945  matunitlindflem2  37949  poimirlem4  37956  poimirlem11  37963  poimirlem12  37964  poimirlem13  37965  poimirlem25  37977  poimirlem28  37980  heicant  37987  mblfinlem2  37990  mblfinlem3  37991  mblfinlem4  37992  mbfposadd  37999  itg2addnclem3  38005  ftc1anclem5  38029  ftc1anclem6  38030  ftc1anclem7  38031  ftc1anc  38033  frinfm  38067  filbcmb  38072  seqpo  38079  sstotbnd2  38106  isbndx  38114  ssbnd  38120  prdsbnd  38125  ismtycnv  38134  ismtyres  38140  heiborlem3  38145  heibor  38153  ghomdiv  38224  grpokerinj  38225  isdrngo2  38290  rngohomco  38306  rngoisocnv  38313  rngoisoco  38314  crngm4  38335  crngohomfo  38338  isidlc  38347  ispridl2  38370  ispridlc  38402  prtlem16  39326  ax12eq  39398  ax12el  39399  lshpcmp  39445  omllaw3  39702  omlfh1N  39715  cvratlem  39878  cvrat3  39899  cvrat4  39900  ps-2  39935  elpaddn0  40257  paddasslem10  40286  cdleme0cp  40671  cdleme32a  40898  cdlemeg49lebilem  40996  cdleme50eq  40998  tendoeq2  41231  diaglbN  41512  diameetN  41513  diainN  41514  dvhopN  41573  djaclN  41593  djajN  41594  dihopelvalcpre  41705  dih1dimatlem  41786  dihmeetcl  41802  djhcl  41857  mapdpglem2  42130  3factsumint1  42471  sticksstones22  42618  unitscyglem4  42648  imacrhmcl  42970  frlmsnic  42996  psrmnd  42999  evlselvlem  43030  fsuppind  43034  0prjspn  43072  infdesc  43087  ismrc  43144  eldioph2  43205  lzenom  43213  rexrabdioph  43237  fphpdo  43260  irrapxlem3  43267  elpell14qr2  43305  pell14qrreccl  43307  pell14qrdich  43312  pellfundglb  43328  monotoddzzfi  43385  2nn0ind  43388  jm2.21  43437  jm2.22  43438  dnnumch3  43490  dnwech  43491  fnwe2lem2  43494  hbtlem6  43572  cantnfresb  43767  imo72b2lem1  44611  mnuprdlem1  44714  mnuprdlem2  44715  relpmin  45394  traxext  45419  cncmpmax  45478  disjf1  45628  eliccelioc  45966  fprodexp  46039  fprodabs2  46040  mullimc  46061  mullimcf  46068  islpcn  46082  limsuppnfdlem  46144  liminfval2  46211  xlimmnfvlem1  46275  xlimmnfvlem2  46276  xlimpnfvlem1  46279  xlimpnfvlem2  46280  cncfshift  46317  cncfperiod  46322  fprodcncf  46343  dvnprodlem1  46389  dvnprodlem2  46390  stoweidlem34  46477  stoweidlem48  46491  stoweidlem60  46503  fourierdlem42  46592  fourierdlem60  46609  fourierdlem61  46610  fourierdlem63  46612  fourierdlem65  46614  fourierdlem87  46636  fourierdlem97  46646  elaa2  46677  etransclem46  46723  etransc  46726  salrestss  46804  sge0iunmptlemfi  46856  isomennd  46974  ovnsslelem  47003  ovolval4lem2  47093  smflimlem3  47216  smflimlem4  47217  smflimlem6  47219  smfpimbor1lem1  47241  smflimmpt  47253  smflimsupmpt  47272  smfliminfmpt  47275  fsetsnf1  47497  fcoresf1  47514  fvelsetpreimafv  47844  icceuelpart  47893  prproropf1olem4  47963  fmtnoprmfac2  48027  bgoldbtbndlem2  48279  bgoldbtbndlem3  48280  gpgnbgrvtx0  48547  gpgnbgrvtx1  48548  gpg3nbgrvtx0ALT  48550  gpg3nbgrvtx1  48551  srhmsubcALTV  48798  xpco2  49329  catprs  49483  uppropd  49653  thincciso2  49927  prsthinc  49936  functermc  49980  fulltermc  49983  lmdran  50143  cmdlan  50144  aacllem  50273