Theorem adantrr 727

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  ad2antrl  738  ad2ant2r  757  ad2ant2lr  758  cases2ALT  1059  consensus  1063  3adant3  1144  3ad2antr1  1201  reusv2lem3  5354  axprlem4OLD  5384  otsndisj  5485  otiunsndisj  5486  po2nr  5565  sotric  5581  sotrieq  5582  tz7.7  6366  fmptsnd  7147  fvtp1g  7176  f1cofveqaeqALT  7236  fsnex  7261  isocnv  7308  isores2  7311  isomin  7315  isoini  7316  f1oiso2  7330  ovmpodf  7546  offval  7663  ordsucun  7799  xp1st  7996  cnvf1olem  8082  fnse  8106  sexp2  8119  mpoxopoveq  8192  frrlem3  8262  frrlem13  8272  oalim  8494  omlim  8495  oaass  8523  omordi  8528  omwordri  8534  odi  8541  oen0  8549  oewordri  8555  nnawordi  8584  nnmordi  8594  omabs  8614  coflton  8634  nadd4  8662  erinxp  8766  dom2lem  8966  domssl  8972  mapen  9106  ssenen  9116  ssfiALT  9135  domfi  9150  php  9168  domunfican  9259  mapfien  9347  ordtypelem6  9464  ordtypelem7  9465  card2inf  9496  inf3lem6  9581  cantnfle  9619  cantnflem1b  9634  cantnflem1  9637  wemapwe  9645  ttrclselem2  9674  rankxplim3  9832  fseqenlem2  9974  dfac5lem4  10075  dfac5lem4OLD  10077  dfac2b  10080  cfsuc  10207  cfflb  10209  cofsmo  10219  infpssrlem4  10256  fin4en1  10259  ssfin4  10260  fin23lem26  10275  fin23lem22  10277  fin23lem27  10278  isf34lem4  10327  isf34lem5  10328  fin1a2lem12  10361  axdc3lem2  10401  axdc4lem  10405  ttukeylem6  10464  iundom2g  10490  pwcfsdom  10534  gchen2  10577  gchor  10578  fpwwe2lem6  10587  fpwwe2lem8  10589  fpwwe2lem10  10591  fpwwe2lem11  10592  fpwwe2  10594  pwfseqlem4  10613  gchina  10650  ltexprlem6  10992  prlem936  10998  mul4  11344  2addsub  11437  muladd  11612  ltleadd  11663  leord1  11707  eqord1  11708  ltord2  11709  leord2  11710  eqord2  11711  divmul3  11843  divcan7  11893  divadddiv  11899  lemul2a  12039  lemul12b  12041  ltmuldiv2  12059  ltdivmul  12060  ledivmul  12061  ltdivmul2  12062  lt2mul2div  12063  ledivmul2  12064  lemuldiv2  12066  lt2msq  12070  ltdiv23  12076  lediv23  12077  fimaxre  12129  supadd  12153  supmullem1  12155  cju  12184  zextlt  12640  suprzcl  12646  zmax  12939  xrlttr  13135  xrre3  13167  qbtwnre  13195  xrsupsslem  13303  xrinfmsslem  13304  supxrunb1  13315  supxrunb2  13316  ixxdisj  13357  iooshf  13423  icodisj  13473  iccf1o  13493  modid  13899  modadd1  13911  modmul1  13930  seqf1o  14049  expsub  14116  sqlecan  14215  bcval5  14324  hashmap  14441  hashfacen  14460  seqcoll  14470  swrdswrdlem  14710  swrdccatin2  14735  cshwidxmod  14809  2cshwcshw  14831  cshwcshid  14833  resqreu  15269  lenegsq  15338  limsupbnd2  15500  icco1  15557  rlimresb  15582  rlimsqzlem  15666  rlimsqz  15667  rlimsqz2  15668  caucvgrlem  15690  fsum0diag2  15800  o1fsum  15831  ruclem8  16259  dvdsmulcr  16309  ndvdsadd  16434  bitsshft  16499  lcmdvds  16632  hashdvds  16800  eulerthlem2  16807  phisum  16816  pcqmul  16879  pcmpt  16918  prmreclem3  16944  4sqlem11  16981  0ram  17046  ramub1  17054  invfun  17787  initoeu2lem2  18038  coaval  18091  catcisolem  18133  funcestrcsetclem8  18169  fullestrcsetc  18173  embedsetcestrclem  18179  funcsetcestrclem8  18184  fullsetcestrc  18188  prfcl  18225  prf1st  18226  prf2nd  18227  1st2ndprf  18228  curfuncf  18260  isposd  18344  lubun  18537  isacs3lem  18564  pslem  18594  psss  18602  chnccat  18648  chnpof1  18652  pwsdiagmhm  18855  grpinvid1  19023  grpinvid2  19024  grplcan  19032  grpnpncan0  19068  dfgrp3lem  19070  dfgrp3  19071  grplactcnv  19075  0nsg  19200  eqger  19209  eqg0subg  19227  qus0subgadd  19230  resghm  19262  conjghm  19279  subgga  19330  gaorber  19338  gastacl  19339  orbsta  19343  symgextf1lem  19450  psgnunilem2  19525  odid  19568  odmulg  19586  gexid  19611  odcau  19634  lsmssv  19673  lsmcom2  19685  pj1ghm  19733  frgpuptf  19800  frgpup1  19805  ghmplusg  19876  cyggex2  19927  gsumval3eu  19934  gsumval3  19937  ablfac1eu  20105  pgpfac1lem5  20111  ablsimpgfind  20142  ringurd  20221  srhmsubc  20716  isdomn4  20752  isdrngd  20801  isdrngdOLD  20803  issrngd  20891  lmhmf1o  21100  lmhmima  21101  lmhmpreima  21102  lspextmo  21110  pwssplit2  21114  pwssplit3  21115  lspdisj  21182  islbs3  21212  lbsextlem4  21218  drngnidl  21300  rngqiprngghmlem2  21345  rngqiprnglinlem1  21348  rngqiprngghm  21356  lidldvgen  21391  cnsubrg  21466  znunit  21602  cygznlem3  21608  dsmmsubg  21782  dsmmlss  21783  frlmsslsp  21835  frlmup1  21837  lindfrn  21860  f1lindf  21861  issubassa2  21931  psrbagconf1o  21968  psrgrp  21995  evlslem2  22119  mhplss  22207  psdmul  22218  psdmvr  22221  ply1sclf1  22339  mamuass  22449  dmatmul  22544  dmatsubcl  22545  dmatmulcl  22547  dmatcrng  22549  scmataddcl  22563  scmatsubcl  22564  scmatcrng  22568  mdetunilem2  22660  pm2mpf1  22846  pm2mpghm  22863  eltg2  23005  ntrss  23102  opncldf1  23131  ssnei2  23163  neindisj  23164  restopnb  23222  restntr  23229  tgcmp  23448  hauscmplem  23453  2ndc1stc  23498  2ndcdisj  23503  2ndcomap  23505  restlly  23530  lly1stc  23543  isref  23556  islocfin  23564  comppfsc  23579  txcls  23651  txdis1cn  23682  pthaus  23685  txlm  23695  qtoptop2  23746  qtopomap  23765  kqt0lem  23783  pt1hmeo  23853  ptuncnv  23854  xkocnv  23861  fbasfip  23915  fgabs  23926  fbasrn  23931  elfm2  23995  fmfnfmlem2  24002  fmfnfmlem4  24004  ptcmplem3  24101  ptcmplem4  24102  tsmsres  24191  tsmsxplem1  24200  utoptop  24281  elbl2ps  24436  elbl2  24437  blin  24468  xmeter  24480  xmetresbl  24484  stdbdxmet  24562  metrest  24571  metustexhalf  24603  dscmet  24619  nrmmetd  24621  tngngp2  24699  nmoi2  24777  icccmplem2  24871  reconnlem2  24875  metdstri  24899  metdsle  24900  metdsre  24901  metnrmlem3  24909  fsumcn  24919  icccvx  24999  bndth  25007  evth  25008  reparphti  25046  pi1blem  25088  tcphcph  25286  iscfil2  25315  cfilfcls  25323  iscau4  25328  iscauf  25329  caucfil  25332  cncmet  25371  minveclem7  25484  ovoliunlem1  25551  ovolicc2lem2  25567  ovolicc2lem3  25568  ovolicc2lem4  25569  ovolicc2lem5  25570  ovolicc2  25571  voliunlem3  25601  voliun  25603  ioombl  25614  volivth  25656  ismbfd  25688  ismbf3d  25703  itg1addlem1  25741  i1fadd  25744  itg1addlem4  25748  itg2split  25798  itg2monolem1  25799  itg2gt0  25809  ibllem  25813  itgvallem3  25835  iblposlem  25841  bddiblnc  25891  dvmptfsum  26024  rolle  26039  dvlip  26042  c1liplem1  26045  lhop1  26063  lhop2  26064  dvcvx  26069  dvfsumge  26071  dvfsumrlimge0  26079  dvfsumrlim  26080  dvfsum2  26083  mdegaddle  26121  mdegvscale  26122  mdegmullem  26125  ply1divex  26184  coeeulem  26271  plyco  26288  dgrlt  26313  vieta1  26363  ulmss  26447  ulmdvlem3  26452  iblulm  26457  tanord  26590  eff1olem  26600  logdivlt  26673  logccv  26715  lawcos  26868  xrlimcnp  27020  cxp2limlem  27027  cxp2lim  27028  cxploglim2  27030  divsqrtsumo1  27035  lgambdd  27088  sqff1o  27233  dvdsppwf1o  27237  dvdsflf1o  27238  musum  27242  muinv  27244  fsumdvdsmul  27246  sgmmul  27252  fsumvma  27264  logfac2  27268  chpchtsum  27270  logfacrlim  27275  logexprlim  27276  dchrelbas3  27289  dchrmulcl  27300  bposlem1  27335  lgsdchr  27406  lgsquadlem1  27431  lgsquadlem2  27432  lgsquad2lem2  27436  chebbnd1lem1  27520  chpchtlim  27530  rplogsumlem2  27536  dchrmusum2  27545  dchrvmasumlem1  27546  dchrvmasum2lem  27547  dchrvmasumlem2  27549  dchrvmasumlem3  27550  dchrvmasumiflem2  27553  dchrisum0flb  27561  dchrisum0fno1  27562  rpvmasum2  27563  dchrisum0re  27564  dchrisum0lem1  27567  dchrisum0lem2a  27568  dchrisum0lem2  27569  dchrisum0lem3  27570  rplogsum  27578  mulogsum  27583  mulog2sumlem2  27586  vmalogdivsum2  27589  2vmadivsumlem  27591  selberglem2  27597  selberg3lem1  27608  selberg4lem1  27611  selberg4  27612  pntrsumo1  27616  selberg34r  27622  pntrlog2bndlem1  27628  pntrlog2bndlem2  27629  pntrlog2bndlem3  27630  pntrlog2bndlem4  27631  pntrlog2bndlem5  27632  pntrlog2bndlem6  27634  pntibndlem3  27643  pntlemp  27661  ostthlem1  27678  ostth3  27689  ltsres  27713  noresle  27748  nosupno  27754  nosupbday  27756  noinfno  27769  bday1  27894  cutlt  28012  addsproplem2  28050  negsproplem2  28109  mulsuniflem  28229  mulsunif2lem  28249  precsexlem9  28295  precsexlem10  28296  precsexlem11  28297  om2noseqlt  28379  om2noseqlt2  28380  om2noseqf1o  28381  om2noseqrdg  28384  noseqrdgfn  28386  bdaypw2n0bndlem  28543  bdayfinbndlem1  28547  recut  28574  elreno2  28575  renegscl  28578  ercgrg  28673  oppperpex  28909  axlowdimlem15  29113  axlowdimlem16  29114  axcontlem10  29130  cusgrfilem1  29612  upgriswlk  29797  crctcshwlkn0  29977  wwlksnext  30049  wwlksnextwrd  30053  clwlkclwwlklem2a  30156  wwlksext2clwwlk  30215  grpoidinv  30667  grporcan  30677  grpoinvid1  30687  grpoinvid2  30688  grpolcan  30689  ablo4  30709  nvabs  30831  minvecolem7  31042  htthlem  31076  hvadd4  31195  hvaddsub4  31237  shscli  31476  pjspansn  31736  fh1  31777  fh2  31778  cm2j  31779  chscllem2  31797  spansncvi  31811  5oalem2  31814  5oalem5  31817  5oalem6  31818  3oalem2  31822  hoadd4  31943  cnvunop  32077  bralnfn  32107  eighmorth  32123  hmops  32179  hmopm  32180  adjlnop  32245  adjmul  32251  adjadd  32252  nmopcoi  32254  kbass5  32279  kbass6  32280  hstle  32389  stlesi  32400  mdsl0  32469  mdexchi  32494  atom1d  32512  superpos  32513  cvexchlem  32527  atomli  32541  atcvatlem  32544  chirredlem2  32550  chirredlem3  32551  atcvat4i  32556  mdsymlem1  32562  mdsymlem3  32564  mdsymlem5  32566  mdsymlem6  32567  sumdmdlem  32577  sumdmdlem2  32578  cdj1i  32592  opeldifid  32758  isoun  32864  1stpreimas  32868  f1od2  32881  indf1ofs  33004  ccatf1  33087  archirngz  33329  archiabllem1  33333  archiabllem2c  33335  qusxpid  33509  esum2d  34350  cntmeas  34483  ddemeas  34493  carsgclctunlem1  34574  itgeq12dv  34583  eulerpartlemgc  34619  eulerpartlemb  34625  eulerpartlemgs2  34637  ballotlemfc0  34750  ballotlemfcc  34751  reprss  34871  reprpmtf1o  34880  hgt750lemb  34910  bnj607  35171  fissorduni  35345  derangenlem  35481  subfacp1lem3  35492  subfacp1lem5  35494  cvmliftmolem2  35592  cvmliftlem6  35600  cvmlift2lem5  35617  cvmlift2lem7  35619  cvmlift2lem9  35621  mppspstlem  35881  dfon2lem6  36096  colinbtwnle  36428  finminlem  36638  nn0prpwlem  36642  isfne  36659  neibastop1  36679  neibastop2lem  36680  neibastop3  36682  tailfb  36697  onsuct0  36761  nndivsub  36777  mh-inf3f1  36861  knoppcnlem6  36896  knoppndvlem9  36918  knoppndvlem18  36927  knoppndvlem21  36930  bj-prmoore  37565  bj-finsumval0  37737  rdgeqoa  37824  pibt2  37871  lindsadd  38072  matunitlindflem2  38076  poimirlem4  38083  poimirlem11  38090  poimirlem12  38091  poimirlem13  38092  poimirlem25  38104  poimirlem28  38107  heicant  38114  mblfinlem2  38117  mblfinlem3  38118  mblfinlem4  38119  mbfposadd  38126  itg2addnclem3  38132  ftc1anclem5  38156  ftc1anclem6  38157  ftc1anclem7  38158  ftc1anc  38160  frinfm  38194  filbcmb  38199  seqpo  38206  sstotbnd2  38233  isbndx  38241  ssbnd  38247  prdsbnd  38252  ismtycnv  38261  ismtyres  38267  heiborlem3  38272  heibor  38280  ghomdiv  38351  grpokerinj  38352  isdrngo2  38417  rngohomco  38433  rngoisocnv  38440  rngoisoco  38441  crngm4  38462  crngohomfo  38465  isidlc  38474  ispridl2  38497  ispridlc  38529  prtlem16  39453  ax12eq  39525  ax12el  39526  lshpcmp  39572  omllaw3  39829  omlfh1N  39842  cvratlem  40005  cvrat3  40026  cvrat4  40027  ps-2  40062  elpaddn0  40384  paddasslem10  40413  cdleme0cp  40798  cdleme32a  41025  cdlemeg49lebilem  41123  cdleme50eq  41125  tendoeq2  41358  diaglbN  41639  diameetN  41640  diainN  41641  dvhopN  41700  djaclN  41720  djajN  41721  dihopelvalcpre  41832  dih1dimatlem  41913  dihmeetcl  41929  djhcl  41984  mapdpglem2  42257  3factsumint1  42598  sticksstones22  42745  unitscyglem4  42775  imacrhmcl  43096  frlmsnic  43118  psrmnd  43121  evlselvlem  43130  fsuppind  43132  0prjspn  43170  infdesc  43185  ismrc  43242  eldioph2  43303  lzenom  43311  rexrabdioph  43331  fphpdo  43354  irrapxlem3  43361  elpell14qr2  43399  pell14qrreccl  43401  pell14qrdich  43406  pellfundglb  43422  monotoddzzfi  43479  2nn0ind  43482  jm2.21  43531  jm2.22  43532  dnnumch3  43584  dnwech  43585  fnwe2lem2  43588  hbtlem6  43666  cantnfresb  43861  imo72b2lem1  44705  mnuprdlem1  44808  mnuprdlem2  44809  relpmin  45488  traxext  45513  cncmpmax  45572  disjf1  45721  eliccelioc  46057  fprodexp  46130  fprodabs2  46131  mullimc  46152  mullimcf  46159  islpcn  46173  limsuppnfdlem  46235  liminfval2  46302  xlimmnfvlem1  46366  xlimmnfvlem2  46367  xlimpnfvlem1  46370  xlimpnfvlem2  46371  cncfshift  46408  cncfperiod  46413  fprodcncf  46434  dvnprodlem1  46480  dvnprodlem2  46481  stoweidlem34  46568  stoweidlem48  46582  stoweidlem60  46594  fourierdlem42  46683  fourierdlem60  46700  fourierdlem61  46701  fourierdlem63  46703  fourierdlem65  46705  fourierdlem87  46727  fourierdlem97  46737  elaa2  46768  etransclem46  46814  etransc  46817  salrestss  46895  sge0iunmptlemfi  46947  isomennd  47065  ovnsslelem  47094  ovolval4lem2  47184  smflimlem3  47307  smflimlem4  47308  smflimlem6  47310  smfpimbor1lem1  47332  smflimmpt  47344  smflimsupmpt  47363  smfliminfmpt  47366  fsetsnf1  47606  fcoresf1  47623  fvelsetpreimafv  47953  icceuelpart  48002  prproropf1olem4  48072  fmtnoprmfac2  48136  bgoldbtbndlem2  48388  bgoldbtbndlem3  48389  gpgnbgrvtx0  48656  gpgnbgrvtx1  48657  gpg3nbgrvtx0ALT  48659  gpg3nbgrvtx1  48660  srhmsubcALTV  48907  xpco2  49438  catprs  49592  uppropd  49762  thincciso2  50036  prsthinc  50045  functermc  50089  fulltermc  50092  lmdran  50252  cmdlan  50253  aacllem  50382