Theorem adantrr 717

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 593	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  728  ad2ant2r  747  ad2ant2lr  748  cases2ALT  1048  consensus  1052  3adant3  1132  3ad2antr1  1189  reusv2lem3  5345  axprlem4OLD  5374  otsndisj  5467  otiunsndisj  5468  po2nr  5546  sotric  5562  sotrieq  5563  tz7.7  6343  fmptsnd  7115  fvtp1g  7144  f1cofveqaeqALT  7204  fsnex  7229  isocnv  7276  isores2  7279  isomin  7283  isoini  7284  f1oiso2  7298  ovmpodf  7514  offval  7631  ordsucun  7767  xp1st  7965  cnvf1olem  8052  fnse  8075  sexp2  8088  mpoxopoveq  8161  frrlem3  8230  frrlem13  8240  oalim  8459  omlim  8460  oaass  8488  omordi  8493  omwordri  8499  odi  8506  oen0  8514  oewordri  8520  nnawordi  8549  nnmordi  8559  omabs  8579  coflton  8599  nadd4  8626  erinxp  8728  dom2lem  8929  domssl  8935  mapen  9069  ssenen  9079  ssfiALT  9098  domfi  9113  php  9131  domunfican  9222  mapfien  9311  ordtypelem6  9428  ordtypelem7  9429  card2inf  9460  inf3lem6  9542  cantnfle  9580  cantnflem1b  9595  cantnflem1  9598  wemapwe  9606  ttrclselem2  9635  rankxplim3  9793  fseqenlem2  9935  dfac5lem4  10036  dfac5lem4OLD  10038  dfac2b  10041  cfsuc  10167  cfflb  10169  cofsmo  10179  infpssrlem4  10216  fin4en1  10219  ssfin4  10220  fin23lem26  10235  fin23lem22  10237  fin23lem27  10238  isf34lem4  10287  isf34lem5  10288  fin1a2lem12  10321  axdc3lem2  10361  axdc4lem  10365  ttukeylem6  10424  iundom2g  10450  pwcfsdom  10494  gchen2  10537  gchor  10538  fpwwe2lem6  10547  fpwwe2lem8  10549  fpwwe2lem10  10551  fpwwe2lem11  10552  fpwwe2  10554  pwfseqlem4  10573  gchina  10610  ltexprlem6  10952  prlem936  10958  mul4  11301  2addsub  11394  muladd  11569  ltleadd  11620  leord1  11664  eqord1  11665  ltord2  11666  leord2  11667  eqord2  11668  divmul3  11801  divcan7  11850  divadddiv  11856  lemul2a  11996  lemul12b  11998  ltmuldiv2  12016  ltdivmul  12017  ledivmul  12018  ltdivmul2  12019  lt2mul2div  12020  ledivmul2  12021  lemuldiv2  12023  lt2msq  12027  ltdiv23  12033  lediv23  12034  fimaxre  12086  supadd  12110  supmullem1  12112  cju  12141  zextlt  12566  suprzcl  12572  zmax  12858  xrlttr  13054  xrre3  13086  qbtwnre  13114  xrsupsslem  13222  xrinfmsslem  13223  supxrunb1  13234  supxrunb2  13235  ixxdisj  13276  iooshf  13342  icodisj  13392  iccf1o  13412  modid  13816  modadd1  13828  modmul1  13847  seqf1o  13966  expsub  14033  sqlecan  14132  bcval5  14241  hashmap  14358  hashfacen  14377  seqcoll  14387  swrdswrdlem  14627  swrdccatin2  14652  cshwidxmod  14726  2cshwcshw  14748  cshwcshid  14750  resqreu  15175  lenegsq  15244  limsupbnd2  15406  icco1  15463  rlimresb  15488  rlimsqzlem  15572  rlimsqz  15573  rlimsqz2  15574  caucvgrlem  15596  fsum0diag2  15706  o1fsum  15736  ruclem8  16162  dvdsmulcr  16212  ndvdsadd  16337  bitsshft  16402  lcmdvds  16535  hashdvds  16702  eulerthlem2  16709  phisum  16718  pcqmul  16781  pcmpt  16820  prmreclem3  16846  4sqlem11  16883  0ram  16948  ramub1  16956  invfun  17688  initoeu2lem2  17939  coaval  17992  catcisolem  18034  funcestrcsetclem8  18070  fullestrcsetc  18074  embedsetcestrclem  18080  funcsetcestrclem8  18085  fullsetcestrc  18089  prfcl  18126  prf1st  18127  prf2nd  18128  1st2ndprf  18129  curfuncf  18161  isposd  18245  lubun  18438  isacs3lem  18465  pslem  18495  psss  18503  chnccat  18549  chnpof1  18553  pwsdiagmhm  18756  grpinvid1  18921  grpinvid2  18922  grplcan  18930  grpnpncan0  18966  dfgrp3lem  18968  dfgrp3  18969  grplactcnv  18973  0nsg  19098  eqger  19107  eqg0subg  19125  qus0subgadd  19128  resghm  19161  conjghm  19178  subgga  19229  gaorber  19237  gastacl  19238  orbsta  19242  symgextf1lem  19349  psgnunilem2  19424  odid  19467  odmulg  19485  gexid  19510  odcau  19533  lsmssv  19572  lsmcom2  19584  pj1ghm  19632  frgpuptf  19699  frgpup1  19704  ghmplusg  19775  cyggex2  19826  gsumval3eu  19833  gsumval3  19836  ablfac1eu  20004  pgpfac1lem5  20010  ablsimpgfind  20041  ringurd  20120  srhmsubc  20613  isdomn4  20649  isdrngd  20698  isdrngdOLD  20700  issrngd  20788  lmhmf1o  20998  lmhmima  20999  lmhmpreima  21000  lspextmo  21008  pwssplit2  21012  pwssplit3  21013  lspdisj  21080  islbs3  21110  lbsextlem4  21116  drngnidl  21198  rngqiprngghmlem2  21243  rngqiprnglinlem1  21246  rngqiprngghm  21254  lidldvgen  21289  cnsubrg  21382  znunit  21518  cygznlem3  21524  dsmmsubg  21698  dsmmlss  21699  frlmsslsp  21751  frlmup1  21753  lindfrn  21776  f1lindf  21777  issubassa2  21848  psrbagconf1o  21885  psrgrp  21912  evlslem2  22034  mhplss  22098  psdmul  22109  psdmvr  22112  ply1sclf1  22231  mamuass  22346  dmatmul  22441  dmatsubcl  22442  dmatmulcl  22444  dmatcrng  22446  scmataddcl  22460  scmatsubcl  22461  scmatcrng  22465  mdetunilem2  22557  pm2mpf1  22743  pm2mpghm  22760  eltg2  22902  ntrss  22999  opncldf1  23028  ssnei2  23060  neindisj  23061  restopnb  23119  restntr  23126  tgcmp  23345  hauscmplem  23350  2ndc1stc  23395  2ndcdisj  23400  2ndcomap  23402  restlly  23427  lly1stc  23440  isref  23453  islocfin  23461  comppfsc  23476  txcls  23548  txdis1cn  23579  pthaus  23582  txlm  23592  qtoptop2  23643  qtopomap  23662  kqt0lem  23680  pt1hmeo  23750  ptuncnv  23751  xkocnv  23758  fbasfip  23812  fgabs  23823  fbasrn  23828  elfm2  23892  fmfnfmlem2  23899  fmfnfmlem4  23901  ptcmplem3  23998  ptcmplem4  23999  tsmsres  24088  tsmsxplem1  24097  utoptop  24178  elbl2ps  24333  elbl2  24334  blin  24365  xmeter  24377  xmetresbl  24381  stdbdxmet  24459  metrest  24468  metustexhalf  24500  dscmet  24516  nrmmetd  24518  tngngp2  24596  nmoi2  24674  icccmplem2  24768  reconnlem2  24772  metdstri  24796  metdsle  24797  metdsre  24798  metnrmlem3  24806  fsumcn  24817  icccvx  24904  bndth  24913  evth  24914  reparphti  24952  reparphtiOLD  24953  pi1blem  24995  tcphcph  25193  iscfil2  25222  cfilfcls  25230  iscau4  25235  iscauf  25236  caucfil  25239  cncmet  25278  minveclem7  25391  ovoliunlem1  25459  ovolicc2lem2  25475  ovolicc2lem3  25476  ovolicc2lem4  25477  ovolicc2lem5  25478  ovolicc2  25479  voliunlem3  25509  voliun  25511  ioombl  25522  volivth  25564  ismbfd  25596  ismbf3d  25611  itg1addlem1  25649  i1fadd  25652  itg1addlem4  25656  itg2split  25706  itg2monolem1  25707  itg2gt0  25717  ibllem  25721  itgvallem3  25743  iblposlem  25749  bddiblnc  25799  dvmptfsum  25935  rolle  25950  dvlip  25954  c1liplem1  25957  lhop1  25975  lhop2  25976  dvcvx  25981  dvfsumge  25984  dvfsumrlimge0  25993  dvfsumrlim  25994  dvfsum2  25997  mdegaddle  26035  mdegvscale  26036  mdegmullem  26039  ply1divex  26098  coeeulem  26185  plyco  26202  dgrlt  26228  vieta1  26276  ulmss  26362  ulmdvlem3  26367  iblulm  26372  tanord  26503  eff1olem  26513  logdivlt  26586  logccv  26628  lawcos  26782  xrlimcnp  26934  cxp2limlem  26942  cxp2lim  26943  cxploglim2  26945  divsqrtsumo1  26950  lgambdd  27003  sqff1o  27148  dvdsppwf1o  27152  dvdsflf1o  27153  musum  27157  muinv  27159  fsumdvdsmul  27161  fsumdvdsmulOLD  27163  sgmmul  27168  fsumvma  27180  logfac2  27184  chpchtsum  27186  logfacrlim  27191  logexprlim  27192  dchrelbas3  27205  dchrmulcl  27216  bposlem1  27251  lgsdchr  27322  lgsquadlem1  27347  lgsquadlem2  27348  lgsquad2lem2  27352  chebbnd1lem1  27436  chpchtlim  27446  rplogsumlem2  27452  dchrmusum2  27461  dchrvmasumlem1  27462  dchrvmasum2lem  27463  dchrvmasumlem2  27465  dchrvmasumlem3  27466  dchrvmasumiflem2  27469  dchrisum0flb  27477  dchrisum0fno1  27478  rpvmasum2  27479  dchrisum0re  27480  dchrisum0lem1  27483  dchrisum0lem2a  27484  dchrisum0lem2  27485  dchrisum0lem3  27486  rplogsum  27494  mulogsum  27499  mulog2sumlem2  27502  vmalogdivsum2  27505  2vmadivsumlem  27507  selberglem2  27513  selberg3lem1  27524  selberg4lem1  27527  selberg4  27528  pntrsumo1  27532  selberg34r  27538  pntrlog2bndlem1  27544  pntrlog2bndlem2  27545  pntrlog2bndlem3  27546  pntrlog2bndlem4  27547  pntrlog2bndlem5  27548  pntrlog2bndlem6  27550  pntibndlem3  27559  pntlemp  27577  ostthlem1  27594  ostth3  27605  ltsres  27630  noresle  27665  nosupno  27671  nosupbday  27673  noinfno  27686  bday1  27810  cutlt  27928  addsproplem2  27966  negsproplem2  28025  mulsuniflem  28145  mulsunif2lem  28165  precsexlem9  28211  precsexlem10  28212  precsexlem11  28213  om2noseqlt  28295  om2noseqlt2  28296  om2noseqf1o  28297  om2noseqrdg  28300  noseqrdgfn  28302  bdaypw2n0bndlem  28459  bdayfinbndlem1  28463  recut  28490  elreno2  28491  renegscl  28494  ercgrg  28589  oppperpex  28825  axlowdimlem15  29029  axlowdimlem16  29030  axcontlem10  29046  cusgrfilem1  29529  upgriswlk  29714  crctcshwlkn0  29894  wwlksnext  29966  wwlksnextwrd  29970  clwlkclwwlklem2a  30073  wwlksext2clwwlk  30132  grpoidinv  30583  grporcan  30593  grpoinvid1  30603  grpoinvid2  30604  grpolcan  30605  ablo4  30625  nvabs  30747  minvecolem7  30958  htthlem  30992  hvadd4  31111  hvaddsub4  31153  shscli  31392  pjspansn  31652  fh1  31693  fh2  31694  cm2j  31695  chscllem2  31713  spansncvi  31727  5oalem2  31730  5oalem5  31733  5oalem6  31734  3oalem2  31738  hoadd4  31859  cnvunop  31993  bralnfn  32023  eighmorth  32039  hmops  32095  hmopm  32096  adjlnop  32161  adjmul  32167  adjadd  32168  nmopcoi  32170  kbass5  32195  kbass6  32196  hstle  32305  stlesi  32316  mdsl0  32385  mdexchi  32410  atom1d  32428  superpos  32429  cvexchlem  32443  atomli  32457  atcvatlem  32460  chirredlem2  32466  chirredlem3  32467  atcvat4i  32472  mdsymlem1  32478  mdsymlem3  32480  mdsymlem5  32482  mdsymlem6  32483  sumdmdlem  32493  sumdmdlem2  32494  cdj1i  32508  opeldifid  32674  isoun  32781  1stpreimas  32785  f1od2  32798  indf1ofs  32948  ccatf1  33031  archirngz  33271  archiabllem1  33275  archiabllem2c  33277  qusxpid  33444  esum2d  34250  cntmeas  34383  ddemeas  34393  carsgclctunlem1  34474  itgeq12dv  34483  eulerpartlemgc  34519  eulerpartlemb  34525  eulerpartlemgs2  34537  ballotlemfc0  34650  ballotlemfcc  34651  reprss  34774  reprpmtf1o  34783  hgt750lemb  34813  bnj607  35072  fissorduni  35246  derangenlem  35365  subfacp1lem3  35376  subfacp1lem5  35378  cvmliftmolem2  35476  cvmliftlem6  35484  cvmlift2lem5  35501  cvmlift2lem7  35503  cvmlift2lem9  35505  mppspstlem  35765  dfon2lem6  35980  colinbtwnle  36312  finminlem  36512  nn0prpwlem  36516  isfne  36533  neibastop1  36553  neibastop2lem  36554  neibastop3  36556  tailfb  36571  onsuct0  36635  nndivsub  36651  knoppcnlem6  36698  knoppndvlem9  36720  knoppndvlem18  36729  knoppndvlem21  36732  bj-prmoore  37320  bj-finsumval0  37490  rdgeqoa  37575  pibt2  37622  lindsadd  37814  matunitlindflem2  37818  poimirlem4  37825  poimirlem11  37832  poimirlem12  37833  poimirlem13  37834  poimirlem25  37846  poimirlem28  37849  heicant  37856  mblfinlem2  37859  mblfinlem3  37860  mblfinlem4  37861  mbfposadd  37868  itg2addnclem3  37874  ftc1anclem5  37898  ftc1anclem6  37899  ftc1anclem7  37900  ftc1anc  37902  frinfm  37936  filbcmb  37941  seqpo  37948  sstotbnd2  37975  isbndx  37983  ssbnd  37989  prdsbnd  37994  ismtycnv  38003  ismtyres  38009  heiborlem3  38014  heibor  38022  ghomdiv  38093  grpokerinj  38094  isdrngo2  38159  rngohomco  38175  rngoisocnv  38182  rngoisoco  38183  crngm4  38204  crngohomfo  38207  isidlc  38216  ispridl2  38239  ispridlc  38271  prtlem16  39129  ax12eq  39201  ax12el  39202  lshpcmp  39248  omllaw3  39505  omlfh1N  39518  cvratlem  39681  cvrat3  39702  cvrat4  39703  ps-2  39738  elpaddn0  40060  paddasslem10  40089  cdleme0cp  40474  cdleme32a  40701  cdlemeg49lebilem  40799  cdleme50eq  40801  tendoeq2  41034  diaglbN  41315  diameetN  41316  diainN  41317  dvhopN  41376  djaclN  41396  djajN  41397  dihopelvalcpre  41508  dih1dimatlem  41589  dihmeetcl  41605  djhcl  41660  mapdpglem2  41933  3factsumint1  42275  sticksstones22  42422  unitscyglem4  42452  imacrhmcl  42769  frlmsnic  42795  psrmnd  42798  evlselvlem  42829  fsuppind  42833  0prjspn  42871  infdesc  42886  ismrc  42943  eldioph2  43004  lzenom  43012  rexrabdioph  43036  fphpdo  43059  irrapxlem3  43066  elpell14qr2  43104  pell14qrreccl  43106  pell14qrdich  43111  pellfundglb  43127  monotoddzzfi  43184  2nn0ind  43187  jm2.21  43236  jm2.22  43237  dnnumch3  43289  dnwech  43290  fnwe2lem2  43293  hbtlem6  43371  cantnfresb  43566  imo72b2lem1  44410  mnuprdlem1  44513  mnuprdlem2  44514  relpmin  45193  traxext  45218  cncmpmax  45277  disjf1  45427  eliccelioc  45767  fprodexp  45840  fprodabs2  45841  mullimc  45862  mullimcf  45869  islpcn  45883  limsuppnfdlem  45945  liminfval2  46012  xlimmnfvlem1  46076  xlimmnfvlem2  46077  xlimpnfvlem1  46080  xlimpnfvlem2  46081  cncfshift  46118  cncfperiod  46123  fprodcncf  46144  dvnprodlem1  46190  dvnprodlem2  46191  stoweidlem34  46278  stoweidlem48  46292  stoweidlem60  46304  fourierdlem42  46393  fourierdlem60  46410  fourierdlem61  46411  fourierdlem63  46413  fourierdlem65  46415  fourierdlem87  46437  fourierdlem97  46447  elaa2  46478  etransclem46  46524  etransc  46527  salrestss  46605  sge0iunmptlemfi  46657  isomennd  46775  ovnsslelem  46804  ovolval4lem2  46894  smflimlem3  47017  smflimlem4  47018  smflimlem6  47020  smfpimbor1lem1  47042  smflimmpt  47054  smflimsupmpt  47073  smfliminfmpt  47076  fsetsnf1  47298  fcoresf1  47315  fvelsetpreimafv  47633  icceuelpart  47682  prproropf1olem4  47752  fmtnoprmfac2  47813  bgoldbtbndlem2  48052  bgoldbtbndlem3  48053  gpgnbgrvtx0  48320  gpgnbgrvtx1  48321  gpg3nbgrvtx0ALT  48323  gpg3nbgrvtx1  48324  srhmsubcALTV  48571  xpco2  49102  catprs  49256  uppropd  49426  thincciso2  49700  prsthinc  49709  functermc  49753  fulltermc  49756  lmdran  49916  cmdlan  49917  aacllem  50046