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  5342  axprlem4OLD  5372  otsndisj  5473  otiunsndisj  5474  po2nr  5553  sotric  5569  sotrieq  5570  tz7.7  6349  fmptsnd  7124  fvtp1g  7153  f1cofveqaeqALT  7213  fsnex  7238  isocnv  7285  isores2  7288  isomin  7292  isoini  7293  f1oiso2  7307  ovmpodf  7523  offval  7640  ordsucun  7776  xp1st  7974  cnvf1olem  8060  fnse  8083  sexp2  8096  mpoxopoveq  8169  frrlem3  8238  frrlem13  8248  oalim  8467  omlim  8468  oaass  8496  omordi  8501  omwordri  8507  odi  8514  oen0  8522  oewordri  8528  nnawordi  8557  nnmordi  8567  omabs  8587  coflton  8607  nadd4  8634  erinxp  8738  dom2lem  8939  domssl  8945  mapen  9079  ssenen  9089  ssfiALT  9108  domfi  9123  php  9141  domunfican  9232  mapfien  9321  ordtypelem6  9438  ordtypelem7  9439  card2inf  9470  inf3lem6  9554  cantnfle  9592  cantnflem1b  9607  cantnflem1  9610  wemapwe  9618  ttrclselem2  9647  rankxplim3  9805  fseqenlem2  9947  dfac5lem4  10048  dfac5lem4OLD  10050  dfac2b  10053  cfsuc  10179  cfflb  10181  cofsmo  10191  infpssrlem4  10228  fin4en1  10231  ssfin4  10232  fin23lem26  10247  fin23lem22  10249  fin23lem27  10250  isf34lem4  10299  isf34lem5  10300  fin1a2lem12  10333  axdc3lem2  10373  axdc4lem  10377  ttukeylem6  10436  iundom2g  10462  pwcfsdom  10506  gchen2  10549  gchor  10550  fpwwe2lem6  10559  fpwwe2lem8  10561  fpwwe2lem10  10563  fpwwe2lem11  10564  fpwwe2  10566  pwfseqlem4  10585  gchina  10622  ltexprlem6  10964  prlem936  10970  mul4  11314  2addsub  11407  muladd  11582  ltleadd  11633  leord1  11677  eqord1  11678  ltord2  11679  leord2  11680  eqord2  11681  divmul3  11814  divcan7  11864  divadddiv  11870  lemul2a  12010  lemul12b  12012  ltmuldiv2  12030  ltdivmul  12031  ledivmul  12032  ltdivmul2  12033  lt2mul2div  12034  ledivmul2  12035  lemuldiv2  12037  lt2msq  12041  ltdiv23  12047  lediv23  12048  fimaxre  12100  supadd  12124  supmullem1  12126  cju  12155  zextlt  12603  suprzcl  12609  zmax  12895  xrlttr  13091  xrre3  13123  qbtwnre  13151  xrsupsslem  13259  xrinfmsslem  13260  supxrunb1  13271  supxrunb2  13272  ixxdisj  13313  iooshf  13379  icodisj  13429  iccf1o  13449  modid  13855  modadd1  13867  modmul1  13886  seqf1o  14005  expsub  14072  sqlecan  14171  bcval5  14280  hashmap  14397  hashfacen  14416  seqcoll  14426  swrdswrdlem  14666  swrdccatin2  14691  cshwidxmod  14765  2cshwcshw  14787  cshwcshid  14789  resqreu  15214  lenegsq  15283  limsupbnd2  15445  icco1  15502  rlimresb  15527  rlimsqzlem  15611  rlimsqz  15612  rlimsqz2  15613  caucvgrlem  15635  fsum0diag2  15745  o1fsum  15776  ruclem8  16204  dvdsmulcr  16254  ndvdsadd  16379  bitsshft  16444  lcmdvds  16577  hashdvds  16745  eulerthlem2  16752  phisum  16761  pcqmul  16824  pcmpt  16863  prmreclem3  16889  4sqlem11  16926  0ram  16991  ramub1  16999  invfun  17731  initoeu2lem2  17982  coaval  18035  catcisolem  18077  funcestrcsetclem8  18113  fullestrcsetc  18117  embedsetcestrclem  18123  funcsetcestrclem8  18128  fullsetcestrc  18132  prfcl  18169  prf1st  18170  prf2nd  18171  1st2ndprf  18172  curfuncf  18204  isposd  18288  lubun  18481  isacs3lem  18508  pslem  18538  psss  18546  chnccat  18592  chnpof1  18596  pwsdiagmhm  18799  grpinvid1  18967  grpinvid2  18968  grplcan  18976  grpnpncan0  19012  dfgrp3lem  19014  dfgrp3  19015  grplactcnv  19019  0nsg  19144  eqger  19153  eqg0subg  19171  qus0subgadd  19174  resghm  19207  conjghm  19224  subgga  19275  gaorber  19283  gastacl  19284  orbsta  19288  symgextf1lem  19395  psgnunilem2  19470  odid  19513  odmulg  19531  gexid  19556  odcau  19579  lsmssv  19618  lsmcom2  19630  pj1ghm  19678  frgpuptf  19745  frgpup1  19750  ghmplusg  19821  cyggex2  19872  gsumval3eu  19879  gsumval3  19882  ablfac1eu  20050  pgpfac1lem5  20056  ablsimpgfind  20087  ringurd  20166  srhmsubc  20657  isdomn4  20693  isdrngd  20742  isdrngdOLD  20744  issrngd  20832  lmhmf1o  21041  lmhmima  21042  lmhmpreima  21043  lspextmo  21051  pwssplit2  21055  pwssplit3  21056  lspdisj  21123  islbs3  21153  lbsextlem4  21159  drngnidl  21241  rngqiprngghmlem2  21286  rngqiprnglinlem1  21289  rngqiprngghm  21297  lidldvgen  21332  cnsubrg  21407  znunit  21543  cygznlem3  21549  dsmmsubg  21723  dsmmlss  21724  frlmsslsp  21776  frlmup1  21778  lindfrn  21801  f1lindf  21802  issubassa2  21872  psrbagconf1o  21909  psrgrp  21935  evlslem2  22057  mhplss  22121  psdmul  22132  psdmvr  22135  ply1sclf1  22254  mamuass  22367  dmatmul  22462  dmatsubcl  22463  dmatmulcl  22465  dmatcrng  22467  scmataddcl  22481  scmatsubcl  22482  scmatcrng  22486  mdetunilem2  22578  pm2mpf1  22764  pm2mpghm  22781  eltg2  22923  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  24199  elbl2ps  24354  elbl2  24355  blin  24386  xmeter  24398  xmetresbl  24402  stdbdxmet  24480  metrest  24489  metustexhalf  24521  dscmet  24537  nrmmetd  24539  tngngp2  24617  nmoi2  24695  icccmplem2  24789  reconnlem2  24793  metdstri  24817  metdsle  24818  metdsre  24819  metnrmlem3  24827  fsumcn  24837  icccvx  24917  bndth  24925  evth  24926  reparphti  24964  pi1blem  25006  tcphcph  25204  iscfil2  25233  cfilfcls  25241  iscau4  25246  iscauf  25247  caucfil  25250  cncmet  25289  minveclem7  25402  ovoliunlem1  25469  ovolicc2lem2  25485  ovolicc2lem3  25486  ovolicc2lem4  25487  ovolicc2lem5  25488  ovolicc2  25489  voliunlem3  25519  voliun  25521  ioombl  25532  volivth  25574  ismbfd  25606  ismbf3d  25621  itg1addlem1  25659  i1fadd  25662  itg1addlem4  25666  itg2split  25716  itg2monolem1  25717  itg2gt0  25727  ibllem  25731  itgvallem3  25753  iblposlem  25759  bddiblnc  25809  dvmptfsum  25942  rolle  25957  dvlip  25960  c1liplem1  25963  lhop1  25981  lhop2  25982  dvcvx  25987  dvfsumge  25989  dvfsumrlimge0  25997  dvfsumrlim  25998  dvfsum2  26001  mdegaddle  26039  mdegvscale  26040  mdegmullem  26043  ply1divex  26102  coeeulem  26189  plyco  26206  dgrlt  26231  vieta1  26278  ulmss  26362  ulmdvlem3  26367  iblulm  26372  tanord  26502  eff1olem  26512  logdivlt  26585  logccv  26627  lawcos  26780  xrlimcnp  26932  cxp2limlem  26939  cxp2lim  26940  cxploglim2  26942  divsqrtsumo1  26947  lgambdd  27000  sqff1o  27145  dvdsppwf1o  27149  dvdsflf1o  27150  musum  27154  muinv  27156  fsumdvdsmul  27158  sgmmul  27164  fsumvma  27176  logfac2  27180  chpchtsum  27182  logfacrlim  27187  logexprlim  27188  dchrelbas3  27201  dchrmulcl  27212  bposlem1  27247  lgsdchr  27318  lgsquadlem1  27343  lgsquadlem2  27344  lgsquad2lem2  27348  chebbnd1lem1  27432  chpchtlim  27442  rplogsumlem2  27448  dchrmusum2  27457  dchrvmasumlem1  27458  dchrvmasum2lem  27459  dchrvmasumlem2  27461  dchrvmasumlem3  27462  dchrvmasumiflem2  27465  dchrisum0flb  27473  dchrisum0fno1  27474  rpvmasum2  27475  dchrisum0re  27476  dchrisum0lem1  27479  dchrisum0lem2a  27480  dchrisum0lem2  27481  dchrisum0lem3  27482  rplogsum  27490  mulogsum  27495  mulog2sumlem2  27498  vmalogdivsum2  27501  2vmadivsumlem  27503  selberglem2  27509  selberg3lem1  27520  selberg4lem1  27523  selberg4  27524  pntrsumo1  27528  selberg34r  27534  pntrlog2bndlem1  27540  pntrlog2bndlem2  27541  pntrlog2bndlem3  27542  pntrlog2bndlem4  27543  pntrlog2bndlem5  27544  pntrlog2bndlem6  27546  pntibndlem3  27555  pntlemp  27573  ostthlem1  27590  ostth3  27601  ltsres  27626  noresle  27661  nosupno  27667  nosupbday  27669  noinfno  27682  bday1  27806  cutlt  27924  addsproplem2  27962  negsproplem2  28021  mulsuniflem  28141  mulsunif2lem  28161  precsexlem9  28207  precsexlem10  28208  precsexlem11  28209  om2noseqlt  28291  om2noseqlt2  28292  om2noseqf1o  28293  om2noseqrdg  28296  noseqrdgfn  28298  bdaypw2n0bndlem  28455  bdayfinbndlem1  28459  recut  28486  elreno2  28487  renegscl  28490  ercgrg  28585  oppperpex  28821  axlowdimlem15  29025  axlowdimlem16  29026  axcontlem10  29042  cusgrfilem1  29524  upgriswlk  29709  crctcshwlkn0  29889  wwlksnext  29961  wwlksnextwrd  29965  clwlkclwwlklem2a  30068  wwlksext2clwwlk  30127  grpoidinv  30579  grporcan  30589  grpoinvid1  30599  grpoinvid2  30600  grpolcan  30601  ablo4  30621  nvabs  30743  minvecolem7  30954  htthlem  30988  hvadd4  31107  hvaddsub4  31149  shscli  31388  pjspansn  31648  fh1  31689  fh2  31690  cm2j  31691  chscllem2  31709  spansncvi  31723  5oalem2  31726  5oalem5  31729  5oalem6  31730  3oalem2  31734  hoadd4  31855  cnvunop  31989  bralnfn  32019  eighmorth  32035  hmops  32091  hmopm  32092  adjlnop  32157  adjmul  32163  adjadd  32164  nmopcoi  32166  kbass5  32191  kbass6  32192  hstle  32301  stlesi  32312  mdsl0  32381  mdexchi  32406  atom1d  32424  superpos  32425  cvexchlem  32439  atomli  32453  atcvatlem  32456  chirredlem2  32462  chirredlem3  32463  atcvat4i  32468  mdsymlem1  32474  mdsymlem3  32476  mdsymlem5  32478  mdsymlem6  32479  sumdmdlem  32489  sumdmdlem2  32490  cdj1i  32504  opeldifid  32669  isoun  32775  1stpreimas  32779  f1od2  32792  indf1ofs  32926  ccatf1  33009  archirngz  33250  archiabllem1  33254  archiabllem2c  33256  qusxpid  33423  esum2d  34237  cntmeas  34370  ddemeas  34380  carsgclctunlem1  34461  itgeq12dv  34470  eulerpartlemgc  34506  eulerpartlemb  34512  eulerpartlemgs2  34524  ballotlemfc0  34637  ballotlemfcc  34638  reprss  34761  reprpmtf1o  34770  hgt750lemb  34800  bnj607  35058  fissorduni  35233  derangenlem  35353  subfacp1lem3  35364  subfacp1lem5  35366  cvmliftmolem2  35464  cvmliftlem6  35472  cvmlift2lem5  35489  cvmlift2lem7  35491  cvmlift2lem9  35493  mppspstlem  35753  dfon2lem6  35968  colinbtwnle  36300  finminlem  36500  nn0prpwlem  36504  isfne  36521  neibastop1  36541  neibastop2lem  36542  neibastop3  36544  tailfb  36559  onsuct0  36623  nndivsub  36639  mh-inf3f1  36723  knoppcnlem6  36758  knoppndvlem9  36780  knoppndvlem18  36789  knoppndvlem21  36792  bj-prmoore  37427  bj-finsumval0  37599  rdgeqoa  37686  pibt2  37733  lindsadd  37934  matunitlindflem2  37938  poimirlem4  37945  poimirlem11  37952  poimirlem12  37953  poimirlem13  37954  poimirlem25  37966  poimirlem28  37969  heicant  37976  mblfinlem2  37979  mblfinlem3  37980  mblfinlem4  37981  mbfposadd  37988  itg2addnclem3  37994  ftc1anclem5  38018  ftc1anclem6  38019  ftc1anclem7  38020  ftc1anc  38022  frinfm  38056  filbcmb  38061  seqpo  38068  sstotbnd2  38095  isbndx  38103  ssbnd  38109  prdsbnd  38114  ismtycnv  38123  ismtyres  38129  heiborlem3  38134  heibor  38142  ghomdiv  38213  grpokerinj  38214  isdrngo2  38279  rngohomco  38295  rngoisocnv  38302  rngoisoco  38303  crngm4  38324  crngohomfo  38327  isidlc  38336  ispridl2  38359  ispridlc  38391  prtlem16  39315  ax12eq  39387  ax12el  39388  lshpcmp  39434  omllaw3  39691  omlfh1N  39704  cvratlem  39867  cvrat3  39888  cvrat4  39889  ps-2  39924  elpaddn0  40246  paddasslem10  40275  cdleme0cp  40660  cdleme32a  40887  cdlemeg49lebilem  40985  cdleme50eq  40987  tendoeq2  41220  diaglbN  41501  diameetN  41502  diainN  41503  dvhopN  41562  djaclN  41582  djajN  41583  dihopelvalcpre  41694  dih1dimatlem  41775  dihmeetcl  41791  djhcl  41846  mapdpglem2  42119  3factsumint1  42460  sticksstones22  42607  unitscyglem4  42637  imacrhmcl  42959  frlmsnic  42985  psrmnd  42988  evlselvlem  43019  fsuppind  43023  0prjspn  43061  infdesc  43076  ismrc  43133  eldioph2  43194  lzenom  43202  rexrabdioph  43222  fphpdo  43245  irrapxlem3  43252  elpell14qr2  43290  pell14qrreccl  43292  pell14qrdich  43297  pellfundglb  43313  monotoddzzfi  43370  2nn0ind  43373  jm2.21  43422  jm2.22  43423  dnnumch3  43475  dnwech  43476  fnwe2lem2  43479  hbtlem6  43557  cantnfresb  43752  imo72b2lem1  44596  mnuprdlem1  44699  mnuprdlem2  44700  relpmin  45379  traxext  45404  cncmpmax  45463  disjf1  45613  eliccelioc  45951  fprodexp  46024  fprodabs2  46025  mullimc  46046  mullimcf  46053  islpcn  46067  limsuppnfdlem  46129  liminfval2  46196  xlimmnfvlem1  46260  xlimmnfvlem2  46261  xlimpnfvlem1  46264  xlimpnfvlem2  46265  cncfshift  46302  cncfperiod  46307  fprodcncf  46328  dvnprodlem1  46374  dvnprodlem2  46375  stoweidlem34  46462  stoweidlem48  46476  stoweidlem60  46488  fourierdlem42  46577  fourierdlem60  46594  fourierdlem61  46595  fourierdlem63  46597  fourierdlem65  46599  fourierdlem87  46621  fourierdlem97  46631  elaa2  46662  etransclem46  46708  etransc  46711  salrestss  46789  sge0iunmptlemfi  46841  isomennd  46959  ovnsslelem  46988  ovolval4lem2  47078  smflimlem3  47201  smflimlem4  47202  smflimlem6  47204  smfpimbor1lem1  47226  smflimmpt  47238  smflimsupmpt  47257  smfliminfmpt  47260  fsetsnf1  47500  fcoresf1  47517  fvelsetpreimafv  47847  icceuelpart  47896  prproropf1olem4  47966  fmtnoprmfac2  48030  bgoldbtbndlem2  48282  bgoldbtbndlem3  48283  gpgnbgrvtx0  48550  gpgnbgrvtx1  48551  gpg3nbgrvtx0ALT  48553  gpg3nbgrvtx1  48554  srhmsubcALTV  48801  xpco2  49332  catprs  49486  uppropd  49656  thincciso2  49930  prsthinc  49939  functermc  49983  fulltermc  49986  lmdran  50146  cmdlan  50147  aacllem  50276