Theorem adantrr 715

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

Syntax hints:   → wi 4   ∧ wa 394

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 395

This theorem is referenced by:  ad2antrl  726  ad2ant2r  745  ad2ant2lr  746  cases2ALT  1046  consensus  1050  3adant3  1129  3ad2antr1  1185  reusv2lem3  5400  axprlem4  5426  otsndisj  5521  otiunsndisj  5522  po2nr  5604  sotric  5618  sotrieq  5619  tz7.7  6397  fmptsnd  7178  fvtp1g  7210  f1cofveqaeqALT  7269  fsnex  7292  isocnv  7337  isores2  7340  isomin  7344  isoini  7345  f1oiso2  7359  ovmpodf  7577  offval  7694  ordsucun  7829  xp1st  8026  cnvf1olem  8115  fnse  8138  sexp2  8151  mpoxopoveq  8225  frrlem3  8294  frrlem13  8304  wfrlem3OLD  8331  oalim  8553  omlim  8554  oaass  8582  omordi  8587  omwordri  8593  odi  8600  oen0  8607  oewordri  8613  nnawordi  8642  nnmordi  8652  omabs  8672  coflton  8692  nadd4  8719  erinxp  8810  dom2lem  9013  domssl  9019  mapen  9169  ssenen  9179  ssfiALT  9202  domfi  9220  php  9238  domunfican  9349  mapfien  9438  ordtypelem6  9553  ordtypelem7  9554  card2inf  9585  inf3lem6  9663  cantnfle  9701  cantnflem1b  9716  cantnflem1  9719  wemapwe  9727  ttrclselem2  9756  rankxplim3  9911  fseqenlem2  10055  dfac5lem4  10156  dfac2b  10160  cfsuc  10287  cfflb  10289  cofsmo  10299  infpssrlem4  10336  fin4en1  10339  ssfin4  10340  fin23lem26  10355  fin23lem22  10357  fin23lem27  10358  isf34lem4  10407  isf34lem5  10408  fin1a2lem12  10441  axdc3lem2  10481  axdc4lem  10485  ttukeylem6  10544  iundom2g  10570  pwcfsdom  10613  gchen2  10656  gchor  10657  fpwwe2lem6  10666  fpwwe2lem8  10668  fpwwe2lem10  10670  fpwwe2lem11  10671  fpwwe2  10673  pwfseqlem4  10692  gchina  10729  ltexprlem6  11071  prlem936  11077  mul4  11419  2addsub  11511  muladd  11683  ltleadd  11734  leord1  11778  eqord1  11779  ltord2  11780  leord2  11781  eqord2  11782  divmul3  11915  divcan7  11961  divadddiv  11967  lemul2a  12107  lemul12b  12109  ltmuldiv2  12126  ltdivmul  12127  ledivmul  12128  ltdivmul2  12129  lt2mul2div  12130  ledivmul2  12131  lemuldiv2  12133  lt2msq  12137  ltdiv23  12143  lediv23  12144  fimaxre  12196  supadd  12220  supmullem1  12222  cju  12246  zextlt  12674  suprzcl  12680  zmax  12967  xrlttr  13159  xrre3  13190  qbtwnre  13218  xrsupsslem  13326  xrinfmsslem  13327  supxrunb1  13338  supxrunb2  13339  ixxdisj  13379  iooshf  13443  icodisj  13493  iccf1o  13513  modid  13902  modadd1  13914  modmul1  13930  seqf1o  14049  expsub  14116  sqlecan  14213  bcval5  14321  hashmap  14438  hashfacen  14457  hashfacenOLD  14458  seqcoll  14469  swrdswrdlem  14698  swrdccatin2  14723  cshwidxmod  14797  2cshwcshw  14820  cshwcshid  14822  resqreu  15243  lenegsq  15311  limsupbnd2  15471  icco1  15528  rlimresb  15553  rlimsqzlem  15639  rlimsqz  15640  rlimsqz2  15641  caucvgrlem  15663  fsum0diag2  15773  o1fsum  15803  ruclem8  16225  dvdsmulcr  16274  ndvdsadd  16398  bitsshft  16461  lcmdvds  16595  hashdvds  16763  eulerthlem2  16770  phisum  16778  pcqmul  16841  pcmpt  16880  prmreclem3  16906  4sqlem11  16943  0ram  17008  ramub1  17016  invfun  17766  initoeu2lem2  18023  coaval  18076  catcisolem  18118  funcestrcsetclem8  18157  fullestrcsetc  18161  embedsetcestrclem  18167  funcsetcestrclem8  18172  fullsetcestrc  18176  prfcl  18213  prf1st  18214  prf2nd  18215  1st2ndprf  18216  curfuncf  18249  isposd  18334  lubun  18526  isacs3lem  18553  pslem  18583  psss  18591  pwsdiagmhm  18807  grpinvid1  18972  grpinvid2  18973  grplcan  18981  grpnpncan0  19016  dfgrp3lem  19018  dfgrp3  19019  grplactcnv  19023  0nsg  19149  eqger  19158  eqg0subg  19176  qus0subgadd  19179  resghm  19212  conjghm  19229  subgga  19280  gaorber  19288  gastacl  19289  orbsta  19293  symgextf1lem  19404  psgnunilem2  19479  odid  19522  odmulg  19540  gexid  19565  odcau  19588  lsmssv  19627  lsmcom2  19639  pj1ghm  19687  frgpuptf  19754  frgpup1  19759  ghmplusg  19830  cyggex2  19881  gsumval3eu  19888  gsumval3  19891  ablfac1eu  20059  pgpfac1lem5  20065  ablsimpgfind  20096  ringurd  20154  srhmsubc  20642  isdrngd  20686  isdrngdOLD  20688  issrngd  20770  lmhmf1o  20960  lmhmima  20961  lmhmpreima  20962  lspextmo  20970  pwssplit2  20974  pwssplit3  20975  lspdisj  21042  islbs3  21072  lbsextlem4  21078  drngnidl  21167  rngqiprngghmlem2  21212  rngqiprnglinlem1  21215  rngqiprngghm  21223  lidldvgen  21258  isdomn4  21284  cnsubrg  21394  znunit  21531  cygznlem3  21537  dsmmsubg  21711  dsmmlss  21712  frlmsslsp  21764  frlmup1  21766  lindfrn  21789  f1lindf  21790  issubassa2  21859  psrbagconf1o  21904  psrbagconf1oOLD  21905  psrgrp  21935  evlslem2  22064  mhplss  22119  psdmul  22130  ply1sclf1  22250  mamuass  22363  dmatmul  22460  dmatsubcl  22461  dmatmulcl  22463  dmatcrng  22465  scmataddcl  22479  scmatsubcl  22480  scmatcrng  22484  mdetunilem2  22576  pm2mpf1  22762  pm2mpghm  22779  eltg2  22922  ntrss  23020  opncldf1  23049  ssnei2  23081  neindisj  23082  restopnb  23140  restntr  23147  tgcmp  23366  hauscmplem  23371  2ndc1stc  23416  2ndcdisj  23421  2ndcomap  23423  restlly  23448  lly1stc  23461  isref  23474  islocfin  23482  comppfsc  23497  txcls  23569  txdis1cn  23600  pthaus  23603  txlm  23613  qtoptop2  23664  qtopomap  23683  kqt0lem  23701  pt1hmeo  23771  ptuncnv  23772  xkocnv  23779  fbasfip  23833  fgabs  23844  fbasrn  23849  elfm2  23913  fmfnfmlem2  23920  fmfnfmlem4  23922  ptcmplem3  24019  ptcmplem4  24020  tsmsres  24109  tsmsxplem1  24118  utoptop  24200  elbl2ps  24356  elbl2  24357  blin  24388  xmeter  24400  xmetresbl  24404  stdbdxmet  24485  metrest  24494  metustexhalf  24526  dscmet  24542  nrmmetd  24544  tngngp2  24630  nmoi2  24708  icccmplem2  24800  reconnlem2  24804  metdstri  24828  metdsle  24829  metdsre  24830  metnrmlem3  24838  fsumcn  24849  icccvx  24936  bndth  24945  evth  24946  reparphti  24984  reparphtiOLD  24985  pi1blem  25027  tcphcph  25226  iscfil2  25255  cfilfcls  25263  iscau4  25268  iscauf  25269  caucfil  25272  cncmet  25311  minveclem7  25424  ovoliunlem1  25492  ovolicc2lem2  25508  ovolicc2lem3  25509  ovolicc2lem4  25510  ovolicc2lem5  25511  ovolicc2  25512  voliunlem3  25542  voliun  25544  ioombl  25555  volivth  25597  ismbfd  25629  ismbf3d  25644  itg1addlem1  25682  i1fadd  25685  itg1addlem4  25689  itg1addlem4OLD  25690  itg2split  25740  itg2monolem1  25741  itg2gt0  25751  ibllem  25755  itgvallem3  25776  iblposlem  25782  bddiblnc  25832  dvmptfsum  25968  rolle  25983  dvlip  25987  c1liplem1  25990  lhop1  26008  lhop2  26009  dvcvx  26014  dvfsumge  26017  dvfsumrlimge0  26026  dvfsumrlim  26027  dvfsum2  26030  mdegaddle  26071  mdegvscale  26072  mdegmullem  26075  ply1divex  26134  coeeulem  26220  plyco  26237  dgrlt  26263  vieta1  26309  ulmss  26395  ulmdvlem3  26400  iblulm  26405  tanord  26534  eff1olem  26544  logdivlt  26617  logccv  26659  lawcos  26813  xrlimcnp  26965  cxp2limlem  26973  cxp2lim  26974  cxploglim2  26976  divsqrtsumo1  26981  lgambdd  27034  sqff1o  27179  dvdsppwf1o  27183  dvdsflf1o  27184  musum  27188  muinv  27190  fsumdvdsmul  27192  fsumdvdsmulOLD  27194  sgmmul  27199  fsumvma  27211  logfac2  27215  chpchtsum  27217  logfacrlim  27222  logexprlim  27223  dchrelbas3  27236  dchrmulcl  27247  bposlem1  27282  lgsdchr  27353  lgsquadlem1  27378  lgsquadlem2  27379  lgsquad2lem2  27383  chebbnd1lem1  27467  chpchtlim  27477  rplogsumlem2  27483  dchrmusum2  27492  dchrvmasumlem1  27493  dchrvmasum2lem  27494  dchrvmasumlem2  27496  dchrvmasumlem3  27497  dchrvmasumiflem2  27500  dchrisum0flb  27508  dchrisum0fno1  27509  rpvmasum2  27510  dchrisum0re  27511  dchrisum0lem1  27514  dchrisum0lem2a  27515  dchrisum0lem2  27516  dchrisum0lem3  27517  rplogsum  27525  mulogsum  27530  mulog2sumlem2  27533  vmalogdivsum2  27536  2vmadivsumlem  27538  selberglem2  27544  selberg3lem1  27555  selberg4lem1  27558  selberg4  27559  pntrsumo1  27563  selberg34r  27569  pntrlog2bndlem1  27575  pntrlog2bndlem2  27576  pntrlog2bndlem3  27577  pntrlog2bndlem4  27578  pntrlog2bndlem5  27579  pntrlog2bndlem6  27581  pntibndlem3  27590  pntlemp  27608  ostthlem1  27625  ostth3  27636  sltres  27661  noresle  27696  nosupno  27702  nosupbday  27704  noinfno  27717  bday1s  27830  cutlt  27918  addsproplem2  27953  negsproplem2  28007  mulsuniflem  28119  mulsunif2lem  28139  precsexlem9  28183  precsexlem10  28184  precsexlem11  28185  om2noseqlt  28242  om2noseqlt2  28243  om2noseqf1o  28244  om2noseqrdg  28247  noseqrdgfn  28249  recut  28316  renegscl  28318  ercgrg  28413  oppperpex  28649  axlowdimlem15  28859  axlowdimlem16  28860  axcontlem10  28876  cusgrfilem1  29361  upgriswlk  29547  crctcshwlkn0  29724  wwlksnext  29796  wwlksnextwrd  29800  clwlkclwwlklem2a  29900  wwlksext2clwwlk  29959  grpoidinv  30410  grporcan  30420  grpoinvid1  30430  grpoinvid2  30431  grpolcan  30432  ablo4  30452  nvabs  30574  minvecolem7  30785  htthlem  30819  hvadd4  30938  hvaddsub4  30980  shscli  31219  pjspansn  31479  fh1  31520  fh2  31521  cm2j  31522  chscllem2  31540  spansncvi  31554  5oalem2  31557  5oalem5  31560  5oalem6  31561  3oalem2  31565  hoadd4  31686  cnvunop  31820  bralnfn  31850  eighmorth  31866  hmops  31922  hmopm  31923  adjlnop  31988  adjmul  31994  adjadd  31995  nmopcoi  31997  kbass5  32022  kbass6  32023  hstle  32132  stlesi  32143  mdsl0  32212  mdexchi  32237  atom1d  32255  superpos  32256  cvexchlem  32270  atomli  32284  atcvatlem  32287  chirredlem2  32293  chirredlem3  32294  atcvat4i  32299  mdsymlem1  32305  mdsymlem3  32307  mdsymlem5  32309  mdsymlem6  32310  sumdmdlem  32320  sumdmdlem2  32321  cdj1i  32335  opeldifid  32488  isoun  32583  1stpreimas  32587  f1od2  32605  ccatf1  32780  archirngz  33010  archiabllem1  33014  archiabllem2c  33016  qusxpid  33195  indf1ofs  33796  esum2d  33863  cntmeas  33996  ddemeas  34006  carsgclctunlem1  34088  itgeq12dv  34097  eulerpartlemgc  34133  eulerpartlemb  34139  eulerpartlemgs2  34151  ballotlemfc0  34263  ballotlemfcc  34264  reprss  34400  reprpmtf1o  34409  hgt750lemb  34439  bnj607  34698  derangenlem  34932  subfacp1lem3  34943  subfacp1lem5  34945  cvmliftmolem2  35043  cvmliftlem6  35051  cvmlift2lem5  35068  cvmlift2lem7  35070  cvmlift2lem9  35072  mppspstlem  35332  dfon2lem6  35535  colinbtwnle  35865  finminlem  35953  nn0prpwlem  35957  isfne  35974  neibastop1  35994  neibastop2lem  35995  neibastop3  35997  tailfb  36012  onsuct0  36076  nndivsub  36092  knoppcnlem6  36124  knoppndvlem9  36146  knoppndvlem18  36155  knoppndvlem21  36158  bj-prmoore  36745  bj-finsumval0  36915  rdgeqoa  37000  pibt2  37047  lindsadd  37237  matunitlindflem2  37241  poimirlem4  37248  poimirlem11  37255  poimirlem12  37256  poimirlem13  37257  poimirlem25  37269  poimirlem28  37272  heicant  37279  mblfinlem2  37282  mblfinlem3  37283  mblfinlem4  37284  mbfposadd  37291  itg2addnclem3  37297  ftc1anclem5  37321  ftc1anclem6  37322  ftc1anclem7  37323  ftc1anc  37325  frinfm  37359  filbcmb  37364  seqpo  37371  sstotbnd2  37398  isbndx  37406  ssbnd  37412  prdsbnd  37417  ismtycnv  37426  ismtyres  37432  heiborlem3  37437  heibor  37445  ghomdiv  37516  grpokerinj  37517  isdrngo2  37582  rngohomco  37598  rngoisocnv  37605  rngoisoco  37606  crngm4  37627  crngohomfo  37630  isidlc  37639  ispridl2  37662  ispridlc  37694  prtlem16  38491  ax12eq  38563  ax12el  38564  lshpcmp  38610  omllaw3  38867  omlfh1N  38880  cvratlem  39044  cvrat3  39065  cvrat4  39066  ps-2  39101  elpaddn0  39423  paddasslem10  39452  cdleme0cp  39837  cdleme32a  40064  cdlemeg49lebilem  40162  cdleme50eq  40164  tendoeq2  40397  diaglbN  40678  diameetN  40679  diainN  40680  dvhopN  40739  djaclN  40759  djajN  40760  dihopelvalcpre  40871  dih1dimatlem  40952  dihmeetcl  40968  djhcl  41023  mapdpglem2  41296  3factsumint1  41644  sticksstones22  41790  metakunt2  41811  imacrhmcl  41908  frlmsnic  41927  psrmnd  41932  evlselvlem  41973  fsuppind  41977  0prjspn  42192  infdesc  42207  ismrc  42268  eldioph2  42329  lzenom  42337  rexrabdioph  42361  fphpdo  42384  irrapxlem3  42391  elpell14qr2  42429  pell14qrreccl  42431  pell14qrdich  42436  pellfundglb  42452  monotoddzzfi  42510  2nn0ind  42513  jm2.21  42562  jm2.22  42563  dnnumch3  42618  dnwech  42619  fnwe2lem2  42622  hbtlem6  42700  cantnfresb  42900  imo72b2lem1  43746  mnuprdlem1  43856  mnuprdlem2  43857  cncmpmax  44541  disjf1  44700  eliccelioc  45049  fprodexp  45125  fprodabs2  45126  mullimc  45147  mullimcf  45154  islpcn  45170  limsuppnfdlem  45232  liminfval2  45299  xlimmnfvlem1  45363  xlimmnfvlem2  45364  xlimpnfvlem1  45367  xlimpnfvlem2  45368  cncfshift  45405  cncfperiod  45410  fprodcncf  45431  dvnprodlem1  45477  dvnprodlem2  45478  stoweidlem34  45565  stoweidlem48  45579  stoweidlem60  45591  fourierdlem42  45680  fourierdlem60  45697  fourierdlem61  45698  fourierdlem63  45700  fourierdlem65  45702  fourierdlem87  45724  fourierdlem97  45734  elaa2  45765  etransclem46  45811  etransc  45814  salrestss  45892  sge0iunmptlemfi  45944  isomennd  46062  ovnsslelem  46091  ovolval4lem2  46181  smflimlem3  46304  smflimlem4  46305  smflimlem6  46307  smfpimbor1lem1  46329  smflimmpt  46341  smflimsupmpt  46360  smfliminfmpt  46363  fsetsnf1  46577  fcoresf1  46594  fvelsetpreimafv  46869  icceuelpart  46918  prproropf1olem4  46988  fmtnoprmfac2  47049  bgoldbtbndlem2  47288  bgoldbtbndlem3  47289  srhmsubcALTV  47578  catprs  48208  prsthinc  48251  aacllem  48425