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 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  726  ad2ant2r  745  ad2ant2lr  746  cases2ALT  1047  consensus  1051  3adant3  1132  3ad2antr1  1188  reusv2lem3  5332  axprlem4  5358  otsndisj  5446  otiunsndisj  5447  po2nr  5528  sotric  5542  sotrieq  5543  tz7.7  6307  fmptsnd  7073  fvtp1g  7105  f1cofveqaeqALT  7164  fsnex  7187  isocnv  7233  isores2  7236  isomin  7240  isoini  7241  f1oiso2  7255  ovmpodf  7461  offval  7574  ordsucun  7704  xp1st  7895  cnvf1olem  7982  fnse  8005  mpoxopoveq  8066  frrlem3  8135  frrlem13  8145  wfrlem3OLD  8172  oalim  8393  omlim  8394  oaass  8423  omordi  8428  omwordri  8434  odi  8441  oen0  8448  oewordri  8454  nnawordi  8483  nnmordi  8493  omabs  8512  erinxp  8611  dom2lem  8813  domssl  8819  mapen  8966  ssenen  8976  ssfiALT  8995  domfi  9013  php  9031  domunfican  9131  mapfien  9211  ordtypelem6  9326  ordtypelem7  9327  card2inf  9358  inf3lem6  9435  cantnfle  9473  cantnflem1b  9488  cantnflem1  9491  wemapwe  9499  ttrclselem2  9528  rankxplim3  9683  fseqenlem2  9827  dfac5lem4  9928  dfac2b  9932  cfsuc  10059  cfflb  10061  cofsmo  10071  infpssrlem4  10108  fin4en1  10111  ssfin4  10112  fin23lem26  10127  fin23lem22  10129  fin23lem27  10130  isf34lem4  10179  isf34lem5  10180  fin1a2lem12  10213  axdc3lem2  10253  axdc4lem  10257  ttukeylem6  10316  iundom2g  10342  pwcfsdom  10385  gchen2  10428  gchor  10429  fpwwe2lem6  10438  fpwwe2lem8  10440  fpwwe2lem10  10442  fpwwe2lem11  10443  fpwwe2  10445  pwfseqlem4  10464  gchina  10501  ltexprlem6  10843  prlem936  10849  mul4  11189  2addsub  11281  muladd  11453  ltleadd  11504  leord1  11548  eqord1  11549  ltord2  11550  leord2  11551  eqord2  11552  divmul3  11684  divcan7  11730  divadddiv  11736  lemul2a  11876  lemul12b  11878  ltmuldiv2  11895  ltdivmul  11896  ledivmul  11897  ltdivmul2  11898  lt2mul2div  11899  ledivmul2  11900  lemuldiv2  11902  lt2msq  11906  ltdiv23  11912  lediv23  11913  fimaxre  11965  supadd  11989  supmullem1  11991  cju  12015  zextlt  12440  suprzcl  12446  zmax  12731  xrlttr  12920  xrre3  12951  qbtwnre  12979  xrsupsslem  13087  xrinfmsslem  13088  supxrunb1  13099  supxrunb2  13100  ixxdisj  13140  iooshf  13204  icodisj  13254  iccf1o  13274  modid  13662  modadd1  13674  modmul1  13690  seqf1o  13810  expsub  13877  sqlecan  13971  bcval5  14078  hashmap  14195  hashfacen  14211  hashfacenOLD  14212  seqcoll  14223  swrdswrdlem  14462  swrdccatin2  14487  cshwidxmod  14561  2cshwcshw  14583  cshwcshid  14585  resqreu  15009  lenegsq  15077  limsupbnd2  15237  icco1  15294  rlimresb  15319  rlimsqzlem  15405  rlimsqz  15406  rlimsqz2  15407  caucvgrlem  15429  fsum0diag2  15540  o1fsum  15570  ruclem8  15991  dvdsmulcr  16040  ndvdsadd  16164  bitsshft  16227  lcmdvds  16358  hashdvds  16521  eulerthlem2  16528  phisum  16536  pcqmul  16599  pcmpt  16638  prmreclem3  16664  4sqlem11  16701  0ram  16766  ramub1  16774  invfun  17521  initoeu2lem2  17775  coaval  17828  catcisolem  17870  funcestrcsetclem8  17909  fullestrcsetc  17913  embedsetcestrclem  17919  funcsetcestrclem8  17924  fullsetcestrc  17928  prfcl  17965  prf1st  17966  prf2nd  17967  1st2ndprf  17968  curfuncf  18001  isposd  18086  lubun  18278  isacs3lem  18305  pslem  18335  psss  18343  pwsdiagmhm  18514  gsumccatOLD  18524  grpinvid1  18675  grpinvid2  18676  grplcan  18682  grpnpncan0  18716  dfgrp3lem  18718  dfgrp3  18719  grplactcnv  18723  0nsg  18842  eqger  18851  resghm  18895  conjghm  18910  subgga  18951  gaorber  18959  gastacl  18960  orbsta  18964  symgextf1lem  19073  psgnunilem2  19148  odid  19191  odmulg  19208  gexid  19231  odcau  19254  lsmssv  19293  lsmcom2  19305  pj1ghm  19354  frgpuptf  19421  frgpup1  19426  ghmplusg  19492  cyggex2  19543  gsumval3eu  19550  gsumval3  19553  ablfac1eu  19721  pgpfac1lem5  19727  ablsimpgfind  19758  isdrngd  20061  issrngd  20166  lmhmf1o  20353  lmhmima  20354  lmhmpreima  20355  lspextmo  20363  pwssplit2  20367  pwssplit3  20368  lspdisj  20432  islbs3  20462  lbsextlem4  20468  drngnidl  20545  lidldvgen  20571  cnsubrg  20703  znunit  20816  cygznlem3  20822  dsmmsubg  20995  dsmmlss  20996  frlmsslsp  21048  frlmup1  21050  lindfrn  21073  f1lindf  21074  issubassa2  21141  psrbagconf1o  21184  psrbagconf1oOLD  21185  evlslem2  21334  mhplss  21390  ply1sclf1  21505  mamuass  21594  dmatmul  21691  dmatsubcl  21692  dmatmulcl  21694  dmatcrng  21696  scmataddcl  21710  scmatsubcl  21711  scmatcrng  21715  mdetunilem2  21807  pm2mpf1  21993  pm2mpghm  22010  eltg2  22153  ntrss  22251  opncldf1  22280  ssnei2  22312  neindisj  22313  restopnb  22371  restntr  22378  tgcmp  22597  hauscmplem  22602  2ndc1stc  22647  2ndcdisj  22652  2ndcomap  22654  restlly  22679  lly1stc  22692  isref  22705  islocfin  22713  comppfsc  22728  txcls  22800  txdis1cn  22831  pthaus  22834  txlm  22844  qtoptop2  22895  qtopomap  22914  kqt0lem  22932  pt1hmeo  23002  ptuncnv  23003  xkocnv  23010  fbasfip  23064  fgabs  23075  fbasrn  23080  elfm2  23144  fmfnfmlem2  23151  fmfnfmlem4  23153  ptcmplem3  23250  ptcmplem4  23251  tsmsres  23340  tsmsxplem1  23349  utoptop  23431  elbl2ps  23587  elbl2  23588  blin  23619  xmeter  23631  xmetresbl  23635  stdbdxmet  23716  metrest  23725  metustexhalf  23757  dscmet  23773  nrmmetd  23775  tngngp2  23861  nmoi2  23939  icccmplem2  24031  reconnlem2  24035  metdstri  24059  metdsle  24060  metdsre  24061  metnrmlem3  24069  fsumcn  24078  icccvx  24158  bndth  24166  evth  24167  reparphti  24205  pi1blem  24247  tcphcph  24446  iscfil2  24475  cfilfcls  24483  iscau4  24488  iscauf  24489  caucfil  24492  cncmet  24531  minveclem7  24644  ovoliunlem1  24711  ovolicc2lem2  24727  ovolicc2lem3  24728  ovolicc2lem4  24729  ovolicc2lem5  24730  ovolicc2  24731  voliunlem3  24761  voliun  24763  ioombl  24774  volivth  24816  ismbfd  24848  ismbf3d  24863  itg1addlem1  24901  i1fadd  24904  itg1addlem4  24908  itg1addlem4OLD  24909  itg2split  24959  itg2monolem1  24960  itg2gt0  24970  ibllem  24974  itgvallem3  24995  iblposlem  25001  bddiblnc  25051  dvmptfsum  25184  rolle  25199  dvlip  25202  c1liplem1  25205  lhop1  25223  lhop2  25224  dvcvx  25229  dvfsumge  25231  dvfsumrlimge0  25239  dvfsumrlim  25240  dvfsum2  25243  mdegaddle  25284  mdegvscale  25285  mdegmullem  25288  ply1divex  25346  coeeulem  25430  plyco  25447  dgrlt  25472  vieta1  25517  ulmss  25601  ulmdvlem3  25606  iblulm  25611  tanord  25739  eff1olem  25749  logdivlt  25821  logccv  25863  lawcos  26011  xrlimcnp  26163  cxp2limlem  26170  cxp2lim  26171  cxploglim2  26173  divsqrtsumo1  26178  lgambdd  26231  sqff1o  26376  dvdsppwf1o  26380  dvdsflf1o  26381  musum  26385  muinv  26387  fsumdvdsmul  26389  sgmmul  26394  fsumvma  26406  logfac2  26410  chpchtsum  26412  logfacrlim  26417  logexprlim  26418  dchrelbas3  26431  dchrmulcl  26442  bposlem1  26477  lgsdchr  26548  lgsquadlem1  26573  lgsquadlem2  26574  lgsquad2lem2  26578  chebbnd1lem1  26662  chpchtlim  26672  rplogsumlem2  26678  dchrmusum2  26687  dchrvmasumlem1  26688  dchrvmasum2lem  26689  dchrvmasumlem2  26691  dchrvmasumlem3  26692  dchrvmasumiflem2  26695  dchrisum0flb  26703  dchrisum0fno1  26704  rpvmasum2  26705  dchrisum0re  26706  dchrisum0lem1  26709  dchrisum0lem2a  26710  dchrisum0lem2  26711  dchrisum0lem3  26712  rplogsum  26720  mulogsum  26725  mulog2sumlem2  26728  vmalogdivsum2  26731  2vmadivsumlem  26733  selberglem2  26739  selberg3lem1  26750  selberg4lem1  26753  selberg4  26754  pntrsumo1  26758  selberg34r  26764  pntrlog2bndlem1  26770  pntrlog2bndlem2  26771  pntrlog2bndlem3  26772  pntrlog2bndlem4  26773  pntrlog2bndlem5  26774  pntrlog2bndlem6  26776  pntibndlem3  26785  pntlemp  26803  ostthlem1  26820  ostth3  26831  ercgrg  26923  oppperpex  27159  axlowdimlem15  27369  axlowdimlem16  27370  axcontlem10  27386  cusgrfilem1  27867  upgriswlk  28053  crctcshwlkn0  28231  wwlksnext  28303  wwlksnextwrd  28307  clwlkclwwlklem2a  28407  wwlksext2clwwlk  28466  grpoidinv  28915  grporcan  28925  grpoinvid1  28935  grpoinvid2  28936  grpolcan  28937  ablo4  28957  nvabs  29079  minvecolem7  29290  htthlem  29324  hvadd4  29443  hvaddsub4  29485  shscli  29724  pjspansn  29984  fh1  30025  fh2  30026  cm2j  30027  chscllem2  30045  spansncvi  30059  5oalem2  30062  5oalem5  30065  5oalem6  30066  3oalem2  30070  hoadd4  30191  cnvunop  30325  bralnfn  30355  eighmorth  30371  hmops  30427  hmopm  30428  adjlnop  30493  adjmul  30499  adjadd  30500  nmopcoi  30502  kbass5  30527  kbass6  30528  hstle  30637  stlesi  30648  mdsl0  30717  mdexchi  30742  atom1d  30760  superpos  30761  cvexchlem  30775  atomli  30789  atcvatlem  30792  chirredlem2  30798  chirredlem3  30799  atcvat4i  30804  mdsymlem1  30810  mdsymlem3  30812  mdsymlem5  30814  mdsymlem6  30815  sumdmdlem  30825  sumdmdlem2  30826  cdj1i  30840  opeldifid  30983  isoun  31079  1stpreimas  31083  f1od2  31101  ccatf1  31268  archirngz  31488  archiabllem1  31492  archiabllem2c  31494  rngurd  31527  qusxpid  31604  indf1ofs  32039  esum2d  32106  cntmeas  32239  ddemeas  32249  carsgclctunlem1  32329  itgeq12dv  32338  eulerpartlemgc  32374  eulerpartlemb  32380  eulerpartlemgs2  32392  ballotlemfc0  32504  ballotlemfcc  32505  reprss  32642  reprpmtf1o  32651  hgt750lemb  32681  bnj607  32941  derangenlem  33178  subfacp1lem3  33189  subfacp1lem5  33191  cvmliftmolem2  33289  cvmliftlem6  33297  cvmlift2lem5  33314  cvmlift2lem7  33316  cvmlift2lem9  33318  mppspstlem  33578  dfon2lem6  33809  sexp2  33838  sltres  33910  noresle  33945  nosupno  33951  nosupbday  33953  noinfno  33966  bday1s  34070  colinbtwnle  34465  finminlem  34552  nn0prpwlem  34556  isfne  34573  neibastop1  34593  neibastop2lem  34594  neibastop3  34596  tailfb  34611  onsuct0  34675  nndivsub  34691  knoppcnlem6  34723  knoppndvlem9  34745  knoppndvlem18  34754  knoppndvlem21  34757  bj-prmoore  35330  bj-finsumval0  35500  rdgeqoa  35585  pibt2  35632  lindsadd  35814  matunitlindflem2  35818  poimirlem4  35825  poimirlem11  35832  poimirlem12  35833  poimirlem13  35834  poimirlem25  35846  poimirlem28  35849  heicant  35856  mblfinlem2  35859  mblfinlem3  35860  mblfinlem4  35861  mbfposadd  35868  itg2addnclem3  35874  ftc1anclem5  35898  ftc1anclem6  35899  ftc1anclem7  35900  ftc1anc  35902  frinfm  35937  filbcmb  35942  seqpo  35949  sstotbnd2  35976  isbndx  35984  ssbnd  35990  prdsbnd  35995  ismtycnv  36004  ismtyres  36010  heiborlem3  36015  heibor  36023  ghomdiv  36094  grpokerinj  36095  isdrngo2  36160  rngohomco  36176  rngoisocnv  36183  rngoisoco  36184  crngm4  36205  crngohomfo  36208  isidlc  36217  ispridl2  36240  ispridlc  36272  prtlem16  36925  ax12eq  36997  ax12el  36998  lshpcmp  37044  omllaw3  37301  omlfh1N  37314  cvratlem  37477  cvrat3  37498  cvrat4  37499  ps-2  37534  elpaddn0  37856  paddasslem10  37885  cdleme0cp  38270  cdleme32a  38497  cdlemeg49lebilem  38595  cdleme50eq  38597  tendoeq2  38830  diaglbN  39111  diameetN  39112  diainN  39113  dvhopN  39172  djaclN  39192  djajN  39193  dihopelvalcpre  39304  dih1dimatlem  39385  dihmeetcl  39401  djhcl  39456  mapdpglem2  39729  3factsumint1  40071  sticksstones22  40166  metakunt2  40168  isdomn4  40214  frlmsnic  40300  fsuppind  40316  mhphf  40322  0prjspn  40502  prjcrv0  40507  infdesc  40517  ismrc  40560  eldioph2  40621  lzenom  40629  rexrabdioph  40653  fphpdo  40676  irrapxlem3  40683  elpell14qr2  40721  pell14qrreccl  40723  pell14qrdich  40728  pellfundglb  40744  monotoddzzfi  40802  2nn0ind  40805  jm2.21  40854  jm2.22  40855  dnnumch3  40910  dnwech  40911  fnwe2lem2  40914  hbtlem6  40992  imo72b2lem1  41818  mnuprdlem1  41928  mnuprdlem2  41929  cncmpmax  42613  disjf1  42764  eliccelioc  43108  fprodexp  43184  fprodabs2  43185  mullimc  43206  mullimcf  43213  islpcn  43229  limsuppnfdlem  43291  liminfval2  43358  xlimmnfvlem1  43422  xlimmnfvlem2  43423  xlimpnfvlem1  43426  xlimpnfvlem2  43427  cncfshift  43464  cncfperiod  43469  fprodcncf  43490  dvnprodlem1  43536  dvnprodlem2  43537  stoweidlem34  43624  stoweidlem48  43638  stoweidlem60  43650  fourierdlem42  43739  fourierdlem60  43756  fourierdlem61  43757  fourierdlem63  43759  fourierdlem65  43761  fourierdlem87  43783  fourierdlem97  43793  elaa2  43824  etransclem46  43870  etransc  43873  salrestss  43949  sge0iunmptlemfi  44001  isomennd  44119  ovnsslelem  44148  ovolval4lem2  44238  smflimlem3  44361  smflimlem4  44362  smflimlem6  44364  smfpimbor1lem1  44386  smflimmpt  44397  smflimsupmpt  44416  smfliminfmpt  44419  fsetsnf1  44604  fcoresf1  44621  fvelsetpreimafv  44897  icceuelpart  44946  prproropf1olem4  45016  fmtnoprmfac2  45077  bgoldbtbndlem2  45316  bgoldbtbndlem3  45317  srhmsubc  45692  srhmsubcALTV  45710  catprs  46350  prsthinc  46393  aacllem  46563