Theorem adantrr 730

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  ad2antrl  741  ad2ant2r  760  ad2ant2lr  761  cases2ALT  1064  consensus  1068  3adant3  1150  3ad2antr1  1207  reusv2lem3  5361  otsndisj  5491  otiunsndisj  5492  po2nr  5572  sotric  5588  sotrieq  5589  tz7.7  6388  fmptsnd  7175  fvtp1g  7204  f1cofveqaeqALT  7263  fsnex  7292  isocnv  7339  isores2  7342  isomin  7346  isoini  7347  f1oiso2  7361  ovmpodf  7577  offval  7703  ordsucun  7837  xp1st  8034  f1od2  8111  cnvf1olem  8124  fnwe2lem3  8150  fnse  8153  sexp2  8166  mpoxopoveq  8240  frrlem3  8310  frrlem13  8320  oalim  8544  omlim  8545  oaass  8573  omordi  8578  omwordri  8584  odi  8591  oen0  8599  oewordri  8605  nnawordi  8634  nnmordi  8644  omabs  8664  coflton  8684  nadd4  8712  erinxp  8816  dom2lem  9023  domssl  9029  mapen  9164  ssenen  9174  ssfiALT  9193  domfi  9208  php  9226  fissorduni  9286  domunfican  9317  mapfien  9404  ordtypelem6  9521  ordtypelem7  9522  card2inf  9553  inf3lem6  9638  cantnfle  9676  cantnflem1b  9691  cantnflem1  9694  wemapwe  9702  ttrclselem2  9731  rankxplim3  9902  fseqenlem2  10108  dfac5lem4  10209  dfac2b  10213  cfsuc  10339  cfflb  10341  cofsmo  10351  infpssrlem4  10388  fin4en1  10391  ssfin4  10392  fin23lem26  10407  fin23lem22  10409  fin23lem27  10410  isf34lem4  10459  isf34lem5  10460  fin1a2lem12  10493  axdc3lem2  10533  axdc4lem  10537  ttukeylem6  10596  iundom2g  10628  pwcfsdom  10672  gchen2  10715  gchor  10716  fpwwe2lem6  10725  fpwwe2lem8  10727  fpwwe2lem10  10729  fpwwe2lem11  10730  fpwwe2  10732  pwfseqlem4  10751  gchina  10788  ltexprlem6  11130  prlem936  11136  mul4  11482  2addsub  11575  muladd  11752  ltleadd  11803  leord1  11847  eqord1  11848  ltord2  11849  leord2  11850  eqord2  11851  divmul3  11983  divcan7  12030  divadddiv  12036  lemul2a  12176  lemul12b  12178  ltmuldiv2  12195  ltdivmul  12196  ledivmul  12197  ltdivmul2  12198  lt2mul2div  12199  ledivmul2  12200  lemuldiv2  12202  lt2msq  12206  ltdiv23  12212  lediv23  12213  fimaxre  12265  supadd  12289  supmullem1  12291  cju  12320  zextlt  12777  suprzcl  12783  zmax  13076  xrlttr  13273  xrre3  13305  qbtwnre  13333  xrsupsslem  13441  xrinfmsslem  13442  supxrunb1  13453  supxrunb2  13454  ixxdisj  13495  iooshf  13561  icodisj  13611  iccf1o  13631  modid  14040  modadd1  14052  modmul1  14071  seqf1o  14190  expsub  14257  sqlecan  14357  bcval5  14466  hashmap  14584  hashfacen  14603  seqcoll  14613  ccatf1  14740  swrdswrdlem  14858  swrdccatin2  14883  cshwidxmod  14959  2cshwcshw  14981  cshwcshid  14983  resqreu  15425  lenegsq  15494  limsupbnd2  15656  icco1  15713  rlimresb  15738  rlimsqzlem  15822  rlimsqz  15823  rlimsqz2  15824  caucvgrlem  15846  fsum0diag2  15955  o1fsum  15986  ruclem8  16411  dvdsmulcr  16461  ndvdsadd  16586  bitsshft  16651  lcmdvds  16789  hashdvds  16958  eulerthlem2  16965  phisum  16974  pcqmul  17037  pcmpt  17076  prmreclem3  17102  4sqlem11  17139  0ram  17204  ramub1  17212  invfun  17945  initoeu2lem2  18196  coaval  18249  catcisolem  18291  funcestrcsetclem8  18327  fullestrcsetc  18331  embedsetcestrclem  18337  funcsetcestrclem8  18342  fullsetcestrc  18346  prfcl  18383  prf1st  18384  prf2nd  18385  1st2ndprf  18386  curfuncf  18418  isposd  18502  lubun  18695  isacs3lem  18722  pslem  18752  psss  18760  chnccat  18806  chnpof1  18810  pwsdiagmhm  19033  grpinvid1  19208  grpinvid2  19209  grplcan  19217  grpnpncan0  19252  dfgrp3lem  19254  dfgrp3  19255  grplactcnv  19259  0nsg  19385  eqger  19396  qusxpid  19401  eqg0subg  19417  qus0subgadd  19420  resghm  19452  conjghm  19469  subgga  19520  gaorber  19528  gastacl  19529  orbsta  19533  symgextf1lem  19640  psgnunilem2  19715  odid  19758  odmulg  19776  gexid  19801  odcau  19824  lsmssv  19863  lsmcom2  19875  pj1ghm  19923  frgpuptf  19990  frgpup1  19995  ghmplusg  20066  cyggex2  20117  gsumval3eu  20124  gsumval3  20127  ablfac1eu  20295  pgpfac1lem5  20301  ablsimpgfind  20332  ringurd  20417  srhmsubc  20938  isdomn4  20973  isdrngd  21028  isdrngdOLD  21030  issrngd  21118  lmhmf1o  21327  lmhmima  21328  lmhmpreima  21329  lspextmo  21337  pwssplit2  21341  pwssplit3  21342  lspdisj  21409  islbs3  21439  lbsextlem4  21445  drngnidl  21537  rngqiprngghmlem2  21590  rngqiprnglinlem1  21593  rngqiprngghm  21601  lidldvgen  21664  cnsubrg  21739  znunit  21875  cygznlem3  21881  dsmmsubg  22055  dsmmlss  22056  frlmsslsp  22108  frlmup1  22110  lindfrn  22133  f1lindf  22134  issubassa2  22206  psrbagconf1o  22243  psrgrp  22270  evlslem2  22394  mhplss  22482  psdmul  22493  psdmvr  22496  ply1sclf1  22614  mamuass  22723  dmatmul  22818  dmatsubcl  22819  dmatmulcl  22821  dmatcrng  22823  scmataddcl  22837  scmatsubcl  22838  scmatcrng  22842  mdetunilem2  22934  matunitlindflem2  23001  pm2mpf1  23123  pm2mpghm  23140  eltg2  23282  ntrss  23379  opncldf1  23408  ssnei2  23440  neindisj  23441  restopnb  23499  restntr  23506  tgcmp  23725  hauscmplem  23730  2ndc1stc  23775  2ndcdisj  23781  2ndcomap  23783  restlly  23808  lly1stc  23821  isref  23834  islocfin  23842  comppfsc  23857  txcls  23929  txdis1cn  23960  pthaus  23963  txlm  23973  qtoptop2  24024  qtopomap  24043  kqt0lem  24061  pt1hmeo  24131  ptuncnv  24132  xkocnv  24139  fbasfip  24193  fgabs  24204  fbasrn  24209  elfm2  24273  fmfnfmlem2  24280  fmfnfmlem4  24282  ptcmplem3  24379  ptcmplem4  24380  tsmsres  24469  tsmsxplem1  24478  utoptop  24559  elbl2ps  24714  elbl2  24715  blin  24746  xmeter  24758  xmetresbl  24762  stdbdxmet  24840  metrest  24849  metustexhalf  24881  dscmet  24897  nrmmetd  24899  tngngp2  24977  nmoi2  25055  icccmplem2  25149  reconnlem2  25153  metdstri  25177  metdsle  25178  metdsre  25179  metnrmlem3  25187  fsumcn  25197  icccvx  25277  bndth  25285  evth  25286  reparphti  25324  pi1blem  25366  tcphcph  25564  iscfil2  25593  cfilfcls  25601  iscau4  25606  iscauf  25607  caucfil  25610  cncmet  25649  minveclem7  25762  ovoliunlem1  25829  ovolicc2lem2  25845  ovolicc2lem3  25846  ovolicc2lem4  25847  ovolicc2lem5  25848  ovolicc2  25849  voliunlem3  25879  voliun  25881  ioombl  25892  volivth  25934  ismbfd  25966  ismbf3d  25981  itg1addlem1  26019  i1fadd  26022  itg1addlem4  26026  itg2split  26076  itg2monolem1  26077  itg2gt0  26087  ibllem  26091  itgvallem3  26112  iblposlem  26118  bddiblnc  26168  dvmptfsum  26301  rolle  26316  dvlip  26319  c1liplem1  26322  lhop1  26340  lhop2  26341  dvcvx  26346  dvfsumge  26348  dvfsumrlimge0  26356  dvfsumrlim  26357  dvfsum2  26360  mdegaddle  26398  mdegvscale  26399  mdegmullem  26402  ply1divex  26461  coeeulem  26549  plyco  26566  dgrlt  26591  vieta1  26641  ulmss  26730  ulmdvlem3  26735  iblulm  26740  tanord  26872  eff1olem  26882  logdivlt  26955  logccv  26997  lawcos  27150  xrlimcnp  27302  cxp2limlem  27309  cxp2lim  27310  cxploglim2  27312  divsqrtsumo1  27317  lgambdd  27370  sqff1o  27515  dvdsppwf1o  27519  dvdsflf1o  27520  musum  27524  muinv  27526  fsumdvdsmul  27528  sgmmul  27534  fsumvma  27546  logfac2  27550  chpchtsum  27552  logfacrlim  27557  logexprlim  27558  dchrelbas3  27571  dchrmulcl  27582  bposlem1  27617  lgsdchr  27688  lgsquadlem1  27713  lgsquadlem2  27714  lgsquad2lem2  27718  chebbnd1lem1  27802  chpchtlim  27812  rplogsumlem2  27818  dchrmusum2  27827  dchrvmasumlem1  27828  dchrvmasum2lem  27829  dchrvmasumlem2  27831  dchrvmasumlem3  27832  dchrvmasumiflem2  27835  dchrisum0flb  27843  dchrisum0fno1  27844  rpvmasum2  27845  dchrisum0re  27846  dchrisum0lem1  27849  dchrisum0lem2a  27850  dchrisum0lem2  27851  dchrisum0lem3  27852  rplogsum  27860  mulogsum  27865  mulog2sumlem2  27868  vmalogdivsum2  27871  2vmadivsumlem  27873  selberglem2  27879  selberg3lem1  27890  selberg4lem1  27893  selberg4  27894  pntrsumo1  27898  selberg34r  27904  pntrlog2bndlem1  27910  pntrlog2bndlem2  27911  pntrlog2bndlem3  27912  pntrlog2bndlem4  27913  pntrlog2bndlem5  27914  pntrlog2bndlem6  27916  pntibndlem3  27925  pntlemp  27943  ostthlem1  27960  ostth3  27971  infdesc  27973  ltsres  28025  noresle  28060  nosupno  28066  nosupbday  28068  noinfno  28081  bday1  28206  cutlt  28324  addsproplem2  28362  negsproplem2  28421  mulsuniflem  28541  mulsunif2lem  28561  precsexlem9  28607  precsexlem10  28608  precsexlem11  28609  om2noseqlt  28691  om2noseqlt2  28692  om2noseqf1o  28693  om2noseqrdg  28696  noseqrdgfn  28698  bdaypw2n0bndlem  28855  bdayfinbndlem1  28859  recut  28886  elreno2  28887  renegscl  28890  ercgrg  28986  oppperpex  29235  axlowdimlem15  29540  axlowdimlem16  29541  axcontlem10  29557  cusgrfilem1  30042  upgriswlk  30227  crctcshwlkn0  30416  wwlksnext  30488  wwlksnextwrd  30492  clwlkclwwlklem2a  30595  wwlksext2clwwlk  30654  grpoidinv  31116  grporcan  31126  grpoinvid1  31136  grpoinvid2  31137  grpolcan  31138  ablo4  31158  nvabs  31280  minvecolem7  31491  htthlem  31525  hvadd4  31644  hvaddsub4  31686  shscli  31925  pjspansn  32185  fh1  32226  fh2  32227  cm2j  32228  chscllem2  32246  spansncvi  32260  5oalem2  32263  5oalem5  32266  5oalem6  32267  3oalem2  32271  hoadd4  32392  cnvunop  32526  bralnfn  32556  eighmorth  32572  hmops  32628  hmopm  32629  adjlnop  32694  adjmul  32700  adjadd  32701  nmopcoi  32703  kbass5  32728  kbass6  32729  hstle  32838  stlesi  32849  mdsl0  32918  mdexchi  32943  atom1d  32961  superpos  32962  cvexchlem  32976  atomli  32990  atcvatlem  32993  chirredlem2  32999  chirredlem3  33000  atcvat4i  33005  mdsymlem1  33011  mdsymlem3  33013  mdsymlem5  33015  mdsymlem6  33016  sumdmdlem  33026  sumdmdlem2  33027  cdj1i  33041  opeldifid  33241  isoun  33343  1stpreimas  33347  indf1ofs  33480  archirngz  33797  archiabllem1  33801  archiabllem2c  33803  esum2d  34772  cntmeas  34906  ddemeas  34916  carsgclctunlem1  34996  itgeq12dv  35005  eulerpartlemgc  35041  eulerpartlemb  35047  eulerpartlemgs2  35059  ballotlemfc0  35172  ballotlemfcc  35173  reprss  35293  reprpmtf1o  35302  hgt750lemb  35332  bnj607  35593  brlexod  35939  brr0d  35941  derangenlem  36023  subfacp1lem3  36034  subfacp1lem5  36036  cvmliftmolem2  36134  cvmliftlem6  36142  cvmlift2lem5  36159  cvmlift2lem7  36161  cvmlift2lem9  36163  mppspstlem  36423  dfon2lem6  36643  colinbtwnle  36976  nmulrid  37039  ltnadd  37060  nadddilem2  37063  nadddilem4  37065  finminlem  37199  nn0prpwlem  37203  isfne  37220  neibastop1  37240  neibastop2lem  37241  neibastop3  37243  tailfb  37258  onsuct0  37322  nndivsub  37338  knoppcnlem6  37457  knoppndvlem9  37479  knoppndvlem18  37488  knoppndvlem21  37491  bj-prmoore  38129  bj-finsumval0  38300  rdgeqoa  38387  pibt2  38434  lindsadd  38630  poimirlem4  38636  poimirlem11  38643  poimirlem12  38644  poimirlem13  38645  poimirlem25  38657  poimirlem28  38660  heicant  38667  mblfinlem2  38670  mblfinlem3  38671  mblfinlem4  38672  mbfposadd  38679  itg2addnclem3  38685  ftc1anclem5  38709  ftc1anclem6  38710  ftc1anclem7  38711  ftc1anc  38713  frinfm  38763  filbcmb  38768  seqpo  38775  sstotbnd2  38802  isbndx  38810  ssbnd  38816  prdsbnd  38821  ismtycnv  38830  ismtyres  38836  heiborlem3  38841  heibor  38849  ghomdiv  38920  grpokerinj  38921  isdrngo2  38986  rngohomco  39002  rngoisocnv  39009  rngoisoco  39010  crngm4  39031  crngohomfo  39034  isidlc  39043  ispridl2  39066  ispridlc  39098  prtlem16  40020  ax12eq  40092  ax12el  40093  lshpcmp  40139  omllaw3  40396  omlfh1N  40409  cvratlem  40572  cvrat3  40593  cvrat4  40594  ps-2  40629  elpaddn0  40951  paddasslem10  40980  cdleme0cp  41365  cdleme32a  41592  cdlemeg49lebilem  41690  cdleme50eq  41692  tendoeq2  41925  diaglbN  42206  diameetN  42207  diainN  42208  dvhopN  42267  djaclN  42287  djajN  42288  dihopelvalcpre  42399  dih1dimatlem  42480  dihmeetcl  42496  djhcl  42551  mapdpglem2  42824  3factsumint1  43165  sticksstones22  43312  unitscyglem4  43342  imacrhmcl  43675  frlmsnic  43698  psrmnd  43701  evlselvlem  43710  fsuppind  43712  0prjspn  43758  ismrc  43806  eldioph2  43867  lzenom  43875  rexrabdioph  43895  fphpdo  43918  irrapxlem3  43925  elpell14qr2  43963  pell14qrreccl  43965  pell14qrdich  43970  pellfundglb  43986  monotoddzzfi  44043  2nn0ind  44046  jm2.21  44095  jm2.22  44096  dnnumch3  44148  dnwech  44149  hbtlem6  44225  cantnfresb  44420  imo72b2lem1  45263  mnuprdlem1  45350  mnuprdlem2  45351  relpmin  46036  traxext  46061  cncmpmax  46143  disjf1  46292  eliccelioc  46627  fprodexp  46700  fprodabs2  46701  mullimc  46722  mullimcf  46729  islpcn  46743  limsuppnfdlem  46805  liminfval2  46872  xlimmnfvlem1  46936  xlimmnfvlem2  46937  xlimpnfvlem1  46940  xlimpnfvlem2  46941  cncfshift  46978  cncfperiod  46983  fprodcncf  47004  dvnprodlem1  47050  dvnprodlem2  47051  stoweidlem34  47138  stoweidlem48  47152  stoweidlem60  47164  fourierdlem42  47253  fourierdlem60  47270  fourierdlem61  47271  fourierdlem63  47273  fourierdlem65  47275  fourierdlem87  47297  fourierdlem97  47307  elaa2  47338  etransclem46  47384  etransc  47387  salrestss  47465  sge0iunmptlemfi  47517  isomennd  47635  ovnsslelem  47664  ovolval4lem2  47754  smflimlem3  47877  smflimlem4  47878  smflimlem6  47880  smfpimbor1lem1  47902  smflimmpt  47914  smflimsupmpt  47933  smfliminfmpt  47936  fsetsnf1  48216  fcoresf1  48233  fvelsetpreimafv  48563  icceuelpart  48612  prproropf1olem4  48682  fmtnoprmfac2  48746  bgoldbtbndlem2  48998  bgoldbtbndlem3  48999  gpgnbgrvtx0  49266  gpgnbgrvtx1  49267  gpg3nbgrvtx0ALT  49269  gpg3nbgrvtx1  49270  srhmsubcALTV  49516  xpco2  50062  catprs  50219  uppropd  50391  thincciso2  50684  prsthinc  50693  functermc  50737  fulltermc  50740  lmdran  50948  cmdlan  50949  aacllem  51108