Theorem adantrr 716

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 484	. 2 ⊢ ((𝜓 ∧ 𝜃) → 𝜓)
2		adant2.1	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3	1, 2	sylan2 594	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  ad2antrl  727  ad2ant2r  746  ad2ant2lr  747  cases2ALT  1048  consensus  1052  3adant3  1133  3ad2antr1  1189  reusv2lem3  5399  axprlem4  5425  otsndisj  5520  otiunsndisj  5521  po2nr  5603  sotric  5617  sotrieq  5618  tz7.7  6391  fmptsnd  7167  fvtp1g  7199  f1cofveqaeqALT  7258  fsnex  7281  isocnv  7327  isores2  7330  isomin  7334  isoini  7335  f1oiso2  7349  ovmpodf  7564  offval  7679  ordsucun  7813  xp1st  8007  cnvf1olem  8096  fnse  8119  sexp2  8132  mpoxopoveq  8204  frrlem3  8273  frrlem13  8283  wfrlem3OLD  8310  oalim  8532  omlim  8533  oaass  8561  omordi  8566  omwordri  8572  odi  8579  oen0  8586  oewordri  8592  nnawordi  8621  nnmordi  8631  omabs  8650  coflton  8670  nadd4  8697  erinxp  8785  dom2lem  8988  domssl  8994  mapen  9141  ssenen  9151  ssfiALT  9174  domfi  9192  php  9210  domunfican  9320  mapfien  9403  ordtypelem6  9518  ordtypelem7  9519  card2inf  9550  inf3lem6  9628  cantnfle  9666  cantnflem1b  9681  cantnflem1  9684  wemapwe  9692  ttrclselem2  9721  rankxplim3  9876  fseqenlem2  10020  dfac5lem4  10121  dfac2b  10125  cfsuc  10252  cfflb  10254  cofsmo  10264  infpssrlem4  10301  fin4en1  10304  ssfin4  10305  fin23lem26  10320  fin23lem22  10322  fin23lem27  10323  isf34lem4  10372  isf34lem5  10373  fin1a2lem12  10406  axdc3lem2  10446  axdc4lem  10450  ttukeylem6  10509  iundom2g  10535  pwcfsdom  10578  gchen2  10621  gchor  10622  fpwwe2lem6  10631  fpwwe2lem8  10633  fpwwe2lem10  10635  fpwwe2lem11  10636  fpwwe2  10638  pwfseqlem4  10657  gchina  10694  ltexprlem6  11036  prlem936  11042  mul4  11382  2addsub  11474  muladd  11646  ltleadd  11697  leord1  11741  eqord1  11742  ltord2  11743  leord2  11744  eqord2  11745  divmul3  11877  divcan7  11923  divadddiv  11929  lemul2a  12069  lemul12b  12071  ltmuldiv2  12088  ltdivmul  12089  ledivmul  12090  ltdivmul2  12091  lt2mul2div  12092  ledivmul2  12093  lemuldiv2  12095  lt2msq  12099  ltdiv23  12105  lediv23  12106  fimaxre  12158  supadd  12182  supmullem1  12184  cju  12208  zextlt  12636  suprzcl  12642  zmax  12929  xrlttr  13119  xrre3  13150  qbtwnre  13178  xrsupsslem  13286  xrinfmsslem  13287  supxrunb1  13298  supxrunb2  13299  ixxdisj  13339  iooshf  13403  icodisj  13453  iccf1o  13473  modid  13861  modadd1  13873  modmul1  13889  seqf1o  14009  expsub  14076  sqlecan  14173  bcval5  14278  hashmap  14395  hashfacen  14413  hashfacenOLD  14414  seqcoll  14425  swrdswrdlem  14654  swrdccatin2  14679  cshwidxmod  14753  2cshwcshw  14776  cshwcshid  14778  resqreu  15199  lenegsq  15267  limsupbnd2  15427  icco1  15484  rlimresb  15509  rlimsqzlem  15595  rlimsqz  15596  rlimsqz2  15597  caucvgrlem  15619  fsum0diag2  15729  o1fsum  15759  ruclem8  16180  dvdsmulcr  16229  ndvdsadd  16353  bitsshft  16416  lcmdvds  16545  hashdvds  16708  eulerthlem2  16715  phisum  16723  pcqmul  16786  pcmpt  16825  prmreclem3  16851  4sqlem11  16888  0ram  16953  ramub1  16961  invfun  17711  initoeu2lem2  17965  coaval  18018  catcisolem  18060  funcestrcsetclem8  18099  fullestrcsetc  18103  embedsetcestrclem  18109  funcsetcestrclem8  18114  fullsetcestrc  18118  prfcl  18155  prf1st  18156  prf2nd  18157  1st2ndprf  18158  curfuncf  18191  isposd  18276  lubun  18468  isacs3lem  18495  pslem  18525  psss  18533  pwsdiagmhm  18712  grpinvid1  18876  grpinvid2  18877  grplcan  18885  grpnpncan0  18919  dfgrp3lem  18921  dfgrp3  18922  grplactcnv  18926  0nsg  19049  eqger  19058  eqg0subg  19073  qus0subgadd  19076  resghm  19108  conjghm  19123  subgga  19164  gaorber  19172  gastacl  19173  orbsta  19177  symgextf1lem  19288  psgnunilem2  19363  odid  19406  odmulg  19424  gexid  19449  odcau  19472  lsmssv  19511  lsmcom2  19523  pj1ghm  19571  frgpuptf  19638  frgpup1  19643  ghmplusg  19714  cyggex2  19765  gsumval3eu  19772  gsumval3  19775  ablfac1eu  19943  pgpfac1lem5  19949  ablsimpgfind  19980  ringurd  20008  isdrngd  20390  isdrngdOLD  20392  issrngd  20469  lmhmf1o  20657  lmhmima  20658  lmhmpreima  20659  lspextmo  20667  pwssplit2  20671  pwssplit3  20672  lspdisj  20738  islbs3  20768  lbsextlem4  20774  drngnidl  20854  lidldvgen  20893  isdomn4  20918  cnsubrg  21005  znunit  21119  cygznlem3  21125  dsmmsubg  21298  dsmmlss  21299  frlmsslsp  21351  frlmup1  21353  lindfrn  21376  f1lindf  21377  issubassa2  21446  psrbagconf1o  21489  psrbagconf1oOLD  21490  psrgrp  21517  evlslem2  21642  mhplss  21698  ply1sclf1  21811  mamuass  21902  dmatmul  21999  dmatsubcl  22000  dmatmulcl  22002  dmatcrng  22004  scmataddcl  22018  scmatsubcl  22019  scmatcrng  22023  mdetunilem2  22115  pm2mpf1  22301  pm2mpghm  22318  eltg2  22461  ntrss  22559  opncldf1  22588  ssnei2  22620  neindisj  22621  restopnb  22679  restntr  22686  tgcmp  22905  hauscmplem  22910  2ndc1stc  22955  2ndcdisj  22960  2ndcomap  22962  restlly  22987  lly1stc  23000  isref  23013  islocfin  23021  comppfsc  23036  txcls  23108  txdis1cn  23139  pthaus  23142  txlm  23152  qtoptop2  23203  qtopomap  23222  kqt0lem  23240  pt1hmeo  23310  ptuncnv  23311  xkocnv  23318  fbasfip  23372  fgabs  23383  fbasrn  23388  elfm2  23452  fmfnfmlem2  23459  fmfnfmlem4  23461  ptcmplem3  23558  ptcmplem4  23559  tsmsres  23648  tsmsxplem1  23657  utoptop  23739  elbl2ps  23895  elbl2  23896  blin  23927  xmeter  23939  xmetresbl  23943  stdbdxmet  24024  metrest  24033  metustexhalf  24065  dscmet  24081  nrmmetd  24083  tngngp2  24169  nmoi2  24247  icccmplem2  24339  reconnlem2  24343  metdstri  24367  metdsle  24368  metdsre  24369  metnrmlem3  24377  fsumcn  24386  icccvx  24466  bndth  24474  evth  24475  reparphti  24513  pi1blem  24555  tcphcph  24754  iscfil2  24783  cfilfcls  24791  iscau4  24796  iscauf  24797  caucfil  24800  cncmet  24839  minveclem7  24952  ovoliunlem1  25019  ovolicc2lem2  25035  ovolicc2lem3  25036  ovolicc2lem4  25037  ovolicc2lem5  25038  ovolicc2  25039  voliunlem3  25069  voliun  25071  ioombl  25082  volivth  25124  ismbfd  25156  ismbf3d  25171  itg1addlem1  25209  i1fadd  25212  itg1addlem4  25216  itg1addlem4OLD  25217  itg2split  25267  itg2monolem1  25268  itg2gt0  25278  ibllem  25282  itgvallem3  25303  iblposlem  25309  bddiblnc  25359  dvmptfsum  25492  rolle  25507  dvlip  25510  c1liplem1  25513  lhop1  25531  lhop2  25532  dvcvx  25537  dvfsumge  25539  dvfsumrlimge0  25547  dvfsumrlim  25548  dvfsum2  25551  mdegaddle  25592  mdegvscale  25593  mdegmullem  25596  ply1divex  25654  coeeulem  25738  plyco  25755  dgrlt  25780  vieta1  25825  ulmss  25909  ulmdvlem3  25914  iblulm  25919  tanord  26047  eff1olem  26057  logdivlt  26129  logccv  26171  lawcos  26321  xrlimcnp  26473  cxp2limlem  26480  cxp2lim  26481  cxploglim2  26483  divsqrtsumo1  26488  lgambdd  26541  sqff1o  26686  dvdsppwf1o  26690  dvdsflf1o  26691  musum  26695  muinv  26697  fsumdvdsmul  26699  sgmmul  26704  fsumvma  26716  logfac2  26720  chpchtsum  26722  logfacrlim  26727  logexprlim  26728  dchrelbas3  26741  dchrmulcl  26752  bposlem1  26787  lgsdchr  26858  lgsquadlem1  26883  lgsquadlem2  26884  lgsquad2lem2  26888  chebbnd1lem1  26972  chpchtlim  26982  rplogsumlem2  26988  dchrmusum2  26997  dchrvmasumlem1  26998  dchrvmasum2lem  26999  dchrvmasumlem2  27001  dchrvmasumlem3  27002  dchrvmasumiflem2  27005  dchrisum0flb  27013  dchrisum0fno1  27014  rpvmasum2  27015  dchrisum0re  27016  dchrisum0lem1  27019  dchrisum0lem2a  27020  dchrisum0lem2  27021  dchrisum0lem3  27022  rplogsum  27030  mulogsum  27035  mulog2sumlem2  27038  vmalogdivsum2  27041  2vmadivsumlem  27043  selberglem2  27049  selberg3lem1  27060  selberg4lem1  27063  selberg4  27064  pntrsumo1  27068  selberg34r  27074  pntrlog2bndlem1  27080  pntrlog2bndlem2  27081  pntrlog2bndlem3  27082  pntrlog2bndlem4  27083  pntrlog2bndlem5  27084  pntrlog2bndlem6  27086  pntibndlem3  27095  pntlemp  27113  ostthlem1  27130  ostth3  27141  sltres  27165  noresle  27200  nosupno  27206  nosupbday  27208  noinfno  27221  bday1s  27332  cutlt  27419  addsproplem2  27454  negsproplem2  27503  mulsuniflem  27604  precsexlem9  27661  precsexlem10  27662  precsexlem11  27663  ercgrg  27768  oppperpex  28004  axlowdimlem15  28214  axlowdimlem16  28215  axcontlem10  28231  cusgrfilem1  28712  upgriswlk  28898  crctcshwlkn0  29075  wwlksnext  29147  wwlksnextwrd  29151  clwlkclwwlklem2a  29251  wwlksext2clwwlk  29310  grpoidinv  29761  grporcan  29771  grpoinvid1  29781  grpoinvid2  29782  grpolcan  29783  ablo4  29803  nvabs  29925  minvecolem7  30136  htthlem  30170  hvadd4  30289  hvaddsub4  30331  shscli  30570  pjspansn  30830  fh1  30871  fh2  30872  cm2j  30873  chscllem2  30891  spansncvi  30905  5oalem2  30908  5oalem5  30911  5oalem6  30912  3oalem2  30916  hoadd4  31037  cnvunop  31171  bralnfn  31201  eighmorth  31217  hmops  31273  hmopm  31274  adjlnop  31339  adjmul  31345  adjadd  31346  nmopcoi  31348  kbass5  31373  kbass6  31374  hstle  31483  stlesi  31494  mdsl0  31563  mdexchi  31588  atom1d  31606  superpos  31607  cvexchlem  31621  atomli  31635  atcvatlem  31638  chirredlem2  31644  chirredlem3  31645  atcvat4i  31650  mdsymlem1  31656  mdsymlem3  31658  mdsymlem5  31660  mdsymlem6  31661  sumdmdlem  31671  sumdmdlem2  31672  cdj1i  31686  opeldifid  31830  isoun  31923  1stpreimas  31927  f1od2  31946  ccatf1  32115  archirngz  32335  archiabllem1  32339  archiabllem2c  32341  qusxpid  32475  indf1ofs  33024  esum2d  33091  cntmeas  33224  ddemeas  33234  carsgclctunlem1  33316  itgeq12dv  33325  eulerpartlemgc  33361  eulerpartlemb  33367  eulerpartlemgs2  33379  ballotlemfc0  33491  ballotlemfcc  33492  reprss  33629  reprpmtf1o  33638  hgt750lemb  33668  bnj607  33927  derangenlem  34162  subfacp1lem3  34173  subfacp1lem5  34175  cvmliftmolem2  34273  cvmliftlem6  34281  cvmlift2lem5  34298  cvmlift2lem7  34300  cvmlift2lem9  34302  mppspstlem  34562  dfon2lem6  34760  colinbtwnle  35090  gg-reparphti  35172  finminlem  35203  nn0prpwlem  35207  isfne  35224  neibastop1  35244  neibastop2lem  35245  neibastop3  35247  tailfb  35262  onsuct0  35326  nndivsub  35342  knoppcnlem6  35374  knoppndvlem9  35396  knoppndvlem18  35405  knoppndvlem21  35408  bj-prmoore  35996  bj-finsumval0  36166  rdgeqoa  36251  pibt2  36298  lindsadd  36481  matunitlindflem2  36485  poimirlem4  36492  poimirlem11  36499  poimirlem12  36500  poimirlem13  36501  poimirlem25  36513  poimirlem28  36516  heicant  36523  mblfinlem2  36526  mblfinlem3  36527  mblfinlem4  36528  mbfposadd  36535  itg2addnclem3  36541  ftc1anclem5  36565  ftc1anclem6  36566  ftc1anclem7  36567  ftc1anc  36569  frinfm  36603  filbcmb  36608  seqpo  36615  sstotbnd2  36642  isbndx  36650  ssbnd  36656  prdsbnd  36661  ismtycnv  36670  ismtyres  36676  heiborlem3  36681  heibor  36689  ghomdiv  36760  grpokerinj  36761  isdrngo2  36826  rngohomco  36842  rngoisocnv  36849  rngoisoco  36850  crngm4  36871  crngohomfo  36874  isidlc  36883  ispridl2  36906  ispridlc  36938  prtlem16  37739  ax12eq  37811  ax12el  37812  lshpcmp  37858  omllaw3  38115  omlfh1N  38128  cvratlem  38292  cvrat3  38313  cvrat4  38314  ps-2  38349  elpaddn0  38671  paddasslem10  38700  cdleme0cp  39085  cdleme32a  39312  cdlemeg49lebilem  39410  cdleme50eq  39412  tendoeq2  39645  diaglbN  39926  diameetN  39927  diainN  39928  dvhopN  39987  djaclN  40007  djajN  40008  dihopelvalcpre  40119  dih1dimatlem  40200  dihmeetcl  40216  djhcl  40271  mapdpglem2  40544  3factsumint1  40886  sticksstones22  40984  metakunt2  40986  imacrhmcl  41089  frlmsnic  41110  evlselvlem  41158  fsuppind  41162  0prjspn  41370  infdesc  41385  ismrc  41439  eldioph2  41500  lzenom  41508  rexrabdioph  41532  fphpdo  41555  irrapxlem3  41562  elpell14qr2  41600  pell14qrreccl  41602  pell14qrdich  41607  pellfundglb  41623  monotoddzzfi  41681  2nn0ind  41684  jm2.21  41733  jm2.22  41734  dnnumch3  41789  dnwech  41790  fnwe2lem2  41793  hbtlem6  41871  cantnfresb  42074  imo72b2lem1  42921  mnuprdlem1  43031  mnuprdlem2  43032  cncmpmax  43716  disjf1  43880  eliccelioc  44234  fprodexp  44310  fprodabs2  44311  mullimc  44332  mullimcf  44339  islpcn  44355  limsuppnfdlem  44417  liminfval2  44484  xlimmnfvlem1  44548  xlimmnfvlem2  44549  xlimpnfvlem1  44552  xlimpnfvlem2  44553  cncfshift  44590  cncfperiod  44595  fprodcncf  44616  dvnprodlem1  44662  dvnprodlem2  44663  stoweidlem34  44750  stoweidlem48  44764  stoweidlem60  44776  fourierdlem42  44865  fourierdlem60  44882  fourierdlem61  44883  fourierdlem63  44885  fourierdlem65  44887  fourierdlem87  44909  fourierdlem97  44919  elaa2  44950  etransclem46  44996  etransc  44999  salrestss  45077  sge0iunmptlemfi  45129  isomennd  45247  ovnsslelem  45276  ovolval4lem2  45366  smflimlem3  45489  smflimlem4  45490  smflimlem6  45492  smfpimbor1lem1  45514  smflimmpt  45526  smflimsupmpt  45545  smfliminfmpt  45548  fsetsnf1  45762  fcoresf1  45779  fvelsetpreimafv  46055  icceuelpart  46104  prproropf1olem4  46174  fmtnoprmfac2  46235  bgoldbtbndlem2  46474  bgoldbtbndlem3  46475  rngqiprngghmlem2  46773  rngqiprnglinlem1  46776  rngqiprngghm  46784  srhmsubc  46974  srhmsubcALTV  46992  catprs  47631  prsthinc  47674  aacllem  47848