Theorem adantrr 729

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  ad2antrl  740  ad2ant2r  759  ad2ant2lr  760  cases2ALT  1062  consensus  1066  3adant3  1148  3ad2antr1  1205  reusv2lem3  5369  axprlem4OLD  5399  otsndisj  5500  otiunsndisj  5501  po2nr  5581  sotric  5597  sotrieq  5598  tz7.7  6383  fmptsnd  7165  fvtp1g  7194  f1cofveqaeqALT  7254  fsnex  7279  isocnv  7326  isores2  7329  isomin  7333  isoini  7334  f1oiso2  7348  ovmpodf  7564  offval  7681  ordsucun  7817  xp1st  8014  cnvf1olem  8101  fnse  8125  sexp2  8138  mpoxopoveq  8211  frrlem3  8281  frrlem13  8291  oalim  8513  omlim  8514  oaass  8542  omordi  8547  omwordri  8553  odi  8560  oen0  8568  oewordri  8574  nnawordi  8603  nnmordi  8613  omabs  8633  coflton  8653  nadd4  8681  erinxp  8785  dom2lem  8985  domssl  8991  mapen  9125  ssenen  9135  ssfiALT  9154  domfi  9169  php  9187  domunfican  9277  mapfien  9364  ordtypelem6  9481  ordtypelem7  9482  card2inf  9513  inf3lem6  9598  cantnfle  9636  cantnflem1b  9651  cantnflem1  9654  wemapwe  9662  ttrclselem2  9691  rankxplim3  9849  fseqenlem2  10005  dfac5lem4  10106  dfac2b  10110  cfsuc  10237  cfflb  10239  cofsmo  10249  infpssrlem4  10286  fin4en1  10289  ssfin4  10290  fin23lem26  10305  fin23lem22  10307  fin23lem27  10308  isf34lem4  10357  isf34lem5  10358  fin1a2lem12  10391  axdc3lem2  10431  axdc4lem  10435  ttukeylem6  10494  iundom2g  10520  pwcfsdom  10564  gchen2  10607  gchor  10608  fpwwe2lem6  10617  fpwwe2lem8  10619  fpwwe2lem10  10621  fpwwe2lem11  10622  fpwwe2  10624  pwfseqlem4  10643  gchina  10680  ltexprlem6  11022  prlem936  11028  mul4  11374  2addsub  11467  muladd  11642  ltleadd  11693  leord1  11737  eqord1  11738  ltord2  11739  leord2  11740  eqord2  11741  divmul3  11873  divcan7  11920  divadddiv  11926  lemul2a  12066  lemul12b  12068  ltmuldiv2  12085  ltdivmul  12086  ledivmul  12087  ltdivmul2  12088  lt2mul2div  12089  ledivmul2  12090  lemuldiv2  12092  lt2msq  12096  ltdiv23  12102  lediv23  12103  fimaxre  12155  supadd  12179  supmullem1  12181  cju  12210  zextlt  12666  suprzcl  12672  zmax  12965  xrlttr  13161  xrre3  13193  qbtwnre  13221  xrsupsslem  13329  xrinfmsslem  13330  supxrunb1  13341  supxrunb2  13342  ixxdisj  13383  iooshf  13449  icodisj  13499  iccf1o  13519  modid  13925  modadd1  13937  modmul1  13956  seqf1o  14075  expsub  14142  sqlecan  14241  bcval5  14350  hashmap  14468  hashfacen  14487  seqcoll  14497  swrdswrdlem  14737  swrdccatin2  14762  cshwidxmod  14836  2cshwcshw  14858  cshwcshid  14860  resqreu  15299  lenegsq  15368  limsupbnd2  15530  icco1  15587  rlimresb  15612  rlimsqzlem  15696  rlimsqz  15697  rlimsqz2  15698  caucvgrlem  15720  fsum0diag2  15830  o1fsum  15861  ruclem8  16289  dvdsmulcr  16339  ndvdsadd  16464  bitsshft  16529  lcmdvds  16662  hashdvds  16830  eulerthlem2  16837  phisum  16846  pcqmul  16909  pcmpt  16948  prmreclem3  16974  4sqlem11  17011  0ram  17076  ramub1  17084  invfun  17817  initoeu2lem2  18068  coaval  18121  catcisolem  18163  funcestrcsetclem8  18199  fullestrcsetc  18203  embedsetcestrclem  18209  funcsetcestrclem8  18214  fullsetcestrc  18218  prfcl  18255  prf1st  18256  prf2nd  18257  1st2ndprf  18258  curfuncf  18290  isposd  18374  lubun  18567  isacs3lem  18594  pslem  18624  psss  18632  chnccat  18678  chnpof1  18682  pwsdiagmhm  18886  grpinvid1  19054  grpinvid2  19055  grplcan  19063  grpnpncan0  19098  dfgrp3lem  19100  dfgrp3  19101  grplactcnv  19105  0nsg  19231  eqger  19242  qusxpid  19247  eqg0subg  19263  qus0subgadd  19266  resghm  19298  conjghm  19315  subgga  19366  gaorber  19374  gastacl  19375  orbsta  19379  symgextf1lem  19486  psgnunilem2  19561  odid  19604  odmulg  19622  gexid  19647  odcau  19670  lsmssv  19709  lsmcom2  19721  pj1ghm  19769  frgpuptf  19836  frgpup1  19841  ghmplusg  19912  cyggex2  19963  gsumval3eu  19970  gsumval3  19973  ablfac1eu  20141  pgpfac1lem5  20147  ablsimpgfind  20178  ringurd  20263  srhmsubc  20761  isdomn4  20796  isdrngd  20843  isdrngdOLD  20845  issrngd  20932  lmhmf1o  21141  lmhmima  21142  lmhmpreima  21143  lspextmo  21151  pwssplit2  21155  pwssplit3  21156  lspdisj  21223  islbs3  21253  lbsextlem4  21259  drngnidl  21347  rngqiprngghmlem2  21395  rngqiprnglinlem1  21398  rngqiprngghm  21406  lidldvgen  21467  cnsubrg  21542  znunit  21678  cygznlem3  21684  dsmmsubg  21858  dsmmlss  21859  frlmsslsp  21911  frlmup1  21913  lindfrn  21936  f1lindf  21937  issubassa2  22007  psrbagconf1o  22044  psrgrp  22071  evlslem2  22195  mhplss  22283  psdmul  22294  psdmvr  22297  ply1sclf1  22415  mamuass  22524  dmatmul  22619  dmatsubcl  22620  dmatmulcl  22622  dmatcrng  22624  scmataddcl  22638  scmatsubcl  22639  scmatcrng  22643  mdetunilem2  22735  pm2mpf1  22921  pm2mpghm  22938  eltg2  23080  ntrss  23177  opncldf1  23206  ssnei2  23238  neindisj  23239  restopnb  23297  restntr  23304  tgcmp  23523  hauscmplem  23528  2ndc1stc  23573  2ndcdisj  23578  2ndcomap  23580  restlly  23605  lly1stc  23618  isref  23631  islocfin  23639  comppfsc  23654  txcls  23726  txdis1cn  23757  pthaus  23760  txlm  23770  qtoptop2  23821  qtopomap  23840  kqt0lem  23858  pt1hmeo  23928  ptuncnv  23929  xkocnv  23936  fbasfip  23990  fgabs  24001  fbasrn  24006  elfm2  24070  fmfnfmlem2  24077  fmfnfmlem4  24079  ptcmplem3  24176  ptcmplem4  24177  tsmsres  24266  tsmsxplem1  24275  utoptop  24356  elbl2ps  24511  elbl2  24512  blin  24543  xmeter  24555  xmetresbl  24559  stdbdxmet  24637  metrest  24646  metustexhalf  24678  dscmet  24694  nrmmetd  24696  tngngp2  24774  nmoi2  24852  icccmplem2  24946  reconnlem2  24950  metdstri  24974  metdsle  24975  metdsre  24976  metnrmlem3  24984  fsumcn  24994  icccvx  25074  bndth  25082  evth  25083  reparphti  25121  pi1blem  25163  tcphcph  25361  iscfil2  25390  cfilfcls  25398  iscau4  25403  iscauf  25404  caucfil  25407  cncmet  25446  minveclem7  25559  ovoliunlem1  25626  ovolicc2lem2  25642  ovolicc2lem3  25643  ovolicc2lem4  25644  ovolicc2lem5  25645  ovolicc2  25646  voliunlem3  25676  voliun  25678  ioombl  25689  volivth  25731  ismbfd  25763  ismbf3d  25778  itg1addlem1  25816  i1fadd  25819  itg1addlem4  25823  itg2split  25873  itg2monolem1  25874  itg2gt0  25884  ibllem  25888  itgvallem3  25910  iblposlem  25916  bddiblnc  25966  dvmptfsum  26099  rolle  26114  dvlip  26117  c1liplem1  26120  lhop1  26138  lhop2  26139  dvcvx  26144  dvfsumge  26146  dvfsumrlimge0  26154  dvfsumrlim  26155  dvfsum2  26158  mdegaddle  26196  mdegvscale  26197  mdegmullem  26200  ply1divex  26259  coeeulem  26346  plyco  26363  dgrlt  26388  vieta1  26438  ulmss  26522  ulmdvlem3  26527  iblulm  26532  tanord  26665  eff1olem  26675  logdivlt  26748  logccv  26790  lawcos  26943  xrlimcnp  27095  cxp2limlem  27102  cxp2lim  27103  cxploglim2  27105  divsqrtsumo1  27110  lgambdd  27163  sqff1o  27308  dvdsppwf1o  27312  dvdsflf1o  27313  musum  27317  muinv  27319  fsumdvdsmul  27321  sgmmul  27327  fsumvma  27339  logfac2  27343  chpchtsum  27345  logfacrlim  27350  logexprlim  27351  dchrelbas3  27364  dchrmulcl  27375  bposlem1  27410  lgsdchr  27481  lgsquadlem1  27506  lgsquadlem2  27507  lgsquad2lem2  27511  chebbnd1lem1  27595  chpchtlim  27605  rplogsumlem2  27611  dchrmusum2  27620  dchrvmasumlem1  27621  dchrvmasum2lem  27622  dchrvmasumlem2  27624  dchrvmasumlem3  27625  dchrvmasumiflem2  27628  dchrisum0flb  27636  dchrisum0fno1  27637  rpvmasum2  27638  dchrisum0re  27639  dchrisum0lem1  27642  dchrisum0lem2a  27643  dchrisum0lem2  27644  dchrisum0lem3  27645  rplogsum  27653  mulogsum  27658  mulog2sumlem2  27661  vmalogdivsum2  27664  2vmadivsumlem  27666  selberglem2  27672  selberg3lem1  27683  selberg4lem1  27686  selberg4  27687  pntrsumo1  27691  selberg34r  27697  pntrlog2bndlem1  27703  pntrlog2bndlem2  27704  pntrlog2bndlem3  27705  pntrlog2bndlem4  27706  pntrlog2bndlem5  27707  pntrlog2bndlem6  27709  pntibndlem3  27718  pntlemp  27736  ostthlem1  27753  ostth3  27764  ltsres  27788  noresle  27823  nosupno  27829  nosupbday  27831  noinfno  27844  bday1  27969  cutlt  28087  addsproplem2  28125  negsproplem2  28184  mulsuniflem  28304  mulsunif2lem  28324  precsexlem9  28370  precsexlem10  28371  precsexlem11  28372  om2noseqlt  28454  om2noseqlt2  28455  om2noseqf1o  28456  om2noseqrdg  28459  noseqrdgfn  28461  bdaypw2n0bndlem  28618  bdayfinbndlem1  28622  recut  28649  elreno2  28650  renegscl  28653  ercgrg  28748  oppperpex  28989  axlowdimlem15  29243  axlowdimlem16  29244  axcontlem10  29260  cusgrfilem1  29742  upgriswlk  29927  crctcshwlkn0  30107  wwlksnext  30179  wwlksnextwrd  30183  clwlkclwwlklem2a  30286  wwlksext2clwwlk  30345  grpoidinv  30797  grporcan  30807  grpoinvid1  30817  grpoinvid2  30818  grpolcan  30819  ablo4  30839  nvabs  30961  minvecolem7  31172  htthlem  31206  hvadd4  31325  hvaddsub4  31367  shscli  31606  pjspansn  31866  fh1  31907  fh2  31908  cm2j  31909  chscllem2  31927  spansncvi  31941  5oalem2  31944  5oalem5  31947  5oalem6  31948  3oalem2  31952  hoadd4  32073  cnvunop  32207  bralnfn  32237  eighmorth  32253  hmops  32309  hmopm  32310  adjlnop  32375  adjmul  32381  adjadd  32382  nmopcoi  32384  kbass5  32409  kbass6  32410  hstle  32519  stlesi  32530  mdsl0  32599  mdexchi  32624  atom1d  32642  superpos  32643  cvexchlem  32657  atomli  32671  atcvatlem  32674  chirredlem2  32680  chirredlem3  32681  atcvat4i  32686  mdsymlem1  32692  mdsymlem3  32694  mdsymlem5  32696  mdsymlem6  32697  sumdmdlem  32707  sumdmdlem2  32708  cdj1i  32722  opeldifid  32881  isoun  32984  1stpreimas  32988  f1od2  33001  indf1ofs  33123  ccatf1  33206  archirngz  33446  archiabllem1  33450  archiabllem2c  33452  esum2d  34424  cntmeas  34557  ddemeas  34567  carsgclctunlem1  34648  itgeq12dv  34657  eulerpartlemgc  34693  eulerpartlemb  34699  eulerpartlemgs2  34711  ballotlemfc0  34824  ballotlemfcc  34825  reprss  34945  reprpmtf1o  34954  hgt750lemb  34984  bnj607  35245  fissorduni  35419  derangenlem  35558  subfacp1lem3  35569  subfacp1lem5  35571  cvmliftmolem2  35669  cvmliftlem6  35677  cvmlift2lem5  35694  cvmlift2lem7  35696  cvmlift2lem9  35698  mppspstlem  35958  dfon2lem6  36173  colinbtwnle  36505  finminlem  36714  nn0prpwlem  36718  isfne  36735  neibastop1  36755  neibastop2lem  36756  neibastop3  36758  tailfb  36773  onsuct0  36837  nndivsub  36853  mh-inf3f1  36937  knoppcnlem6  36972  knoppndvlem9  36994  knoppndvlem18  37003  knoppndvlem21  37006  bj-prmoore  37640  bj-finsumval0  37812  rdgeqoa  37899  pibt2  37946  lindsadd  38147  matunitlindflem2  38151  poimirlem4  38158  poimirlem11  38165  poimirlem12  38166  poimirlem13  38167  poimirlem25  38179  poimirlem28  38182  heicant  38189  mblfinlem2  38192  mblfinlem3  38193  mblfinlem4  38194  mbfposadd  38201  itg2addnclem3  38207  ftc1anclem5  38231  ftc1anclem6  38232  ftc1anclem7  38233  ftc1anc  38235  frinfm  38269  filbcmb  38274  seqpo  38281  sstotbnd2  38308  isbndx  38316  ssbnd  38322  prdsbnd  38327  ismtycnv  38336  ismtyres  38342  heiborlem3  38347  heibor  38355  ghomdiv  38426  grpokerinj  38427  isdrngo2  38492  rngohomco  38508  rngoisocnv  38515  rngoisoco  38516  crngm4  38537  crngohomfo  38540  isidlc  38549  ispridl2  38572  ispridlc  38604  prtlem16  39528  ax12eq  39600  ax12el  39601  lshpcmp  39647  omllaw3  39904  omlfh1N  39917  cvratlem  40080  cvrat3  40101  cvrat4  40102  ps-2  40137  elpaddn0  40459  paddasslem10  40488  cdleme0cp  40873  cdleme32a  41100  cdlemeg49lebilem  41198  cdleme50eq  41200  tendoeq2  41433  diaglbN  41714  diameetN  41715  diainN  41716  dvhopN  41775  djaclN  41795  djajN  41796  dihopelvalcpre  41907  dih1dimatlem  41988  dihmeetcl  42004  djhcl  42059  mapdpglem2  42332  3factsumint1  42673  sticksstones22  42820  unitscyglem4  42850  imacrhmcl  43171  frlmsnic  43193  psrmnd  43196  evlselvlem  43205  fsuppind  43207  0prjspn  43245  infdesc  43260  ismrc  43317  eldioph2  43378  lzenom  43386  rexrabdioph  43406  fphpdo  43429  irrapxlem3  43436  elpell14qr2  43474  pell14qrreccl  43476  pell14qrdich  43481  pellfundglb  43497  monotoddzzfi  43554  2nn0ind  43557  jm2.21  43606  jm2.22  43607  dnnumch3  43659  dnwech  43660  fnwe2lem2  43663  hbtlem6  43741  cantnfresb  43936  imo72b2lem1  44780  mnuprdlem1  44867  mnuprdlem2  44868  relpmin  45546  traxext  45571  cncmpmax  45637  disjf1  45786  eliccelioc  46122  fprodexp  46195  fprodabs2  46196  mullimc  46217  mullimcf  46224  islpcn  46238  limsuppnfdlem  46300  liminfval2  46367  xlimmnfvlem1  46431  xlimmnfvlem2  46432  xlimpnfvlem1  46435  xlimpnfvlem2  46436  cncfshift  46473  cncfperiod  46478  fprodcncf  46499  dvnprodlem1  46545  dvnprodlem2  46546  stoweidlem34  46633  stoweidlem48  46647  stoweidlem60  46659  fourierdlem42  46748  fourierdlem60  46765  fourierdlem61  46766  fourierdlem63  46768  fourierdlem65  46770  fourierdlem87  46792  fourierdlem97  46802  elaa2  46833  etransclem46  46879  etransc  46882  salrestss  46960  sge0iunmptlemfi  47012  isomennd  47130  ovnsslelem  47159  ovolval4lem2  47249  smflimlem3  47372  smflimlem4  47373  smflimlem6  47375  smfpimbor1lem1  47397  smflimmpt  47409  smflimsupmpt  47428  smfliminfmpt  47431  fsetsnf1  47671  fcoresf1  47688  fvelsetpreimafv  48018  icceuelpart  48067  prproropf1olem4  48137  fmtnoprmfac2  48201  bgoldbtbndlem2  48453  bgoldbtbndlem3  48454  gpgnbgrvtx0  48721  gpgnbgrvtx1  48722  gpg3nbgrvtx0ALT  48724  gpg3nbgrvtx1  48725  srhmsubcALTV  48972  xpco2  49513  catprs  49667  uppropd  49837  thincciso2  50111  prsthinc  50120  functermc  50164  fulltermc  50167  lmdran  50327  cmdlan  50328  aacllem  50457