Theorem adantrr 749

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

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  ad2ant2r  779  ad2ant2lr  780  consensus  990  cases2  1005  3ad2antr1  1219  reusv2lem3  4797  otsndisj  4904  otiunsndisj  4905  po2nr  4972  sotric  4985  sotrieq  4986  tz7.7  5666  fmptsnd  6340  fvtp1g  6368  fsnex  6438  isocnv  6480  isores2  6483  isomin  6487  isoini  6488  f1oiso2  6502  ovmpt2df  6690  offval  6802  ordsucun  6917  xp1st  7089  1stconst  7152  cnvf1olem  7162  fnse  7181  mpt2xopoveq  7232  wfrlem3  7303  oalim  7499  omlim  7500  oaass  7528  omordi  7533  omwordri  7539  odi  7546  oen0  7553  oewordri  7559  nnawordi  7588  nnmordi  7598  omabs  7614  erinxp  7708  dom2lem  7881  mapen  8009  ssenen  8019  ssfi  8065  domfi  8066  domunfican  8118  mapfien  8196  ordtypelem6  8311  ordtypelem7  8312  card2inf  8343  inf3lem6  8413  cantnfle  8451  cantnflem1b  8466  cantnflem1  8469  wemapwe  8477  rankxplim3  8627  fseqenlem2  8731  dfac5lem4  8832  dfac2  8836  cfsuc  8962  cfflb  8964  cofsmo  8974  infpssrlem4  9011  fin4en1  9014  ssfin4  9015  fin23lem26  9030  fin23lem22  9032  fin23lem27  9033  isf34lem4  9082  isf34lem5  9083  fin1a2lem12  9116  axdc3lem2  9156  axdc4lem  9160  ttukeylem6  9219  iundom2g  9241  pwcfsdom  9284  gchen2  9327  gchor  9328  fpwwe2lem7  9337  fpwwe2lem9  9339  fpwwe2lem11  9341  fpwwe2lem12  9342  fpwwe2  9344  pwfseqlem4  9363  gchina  9400  ltexprlem6  9742  prlem936  9748  mul4  10084  2addsub  10174  muladd  10341  ltleadd  10390  leord1  10434  eqord1  10435  ltord2  10436  leord2  10437  eqord2  10438  divmul3  10569  divcan7  10613  divadddiv  10619  lemul2a  10757  lemul12b  10759  ltmuldiv2  10776  ltdivmul  10777  ledivmul  10778  ltdivmul2  10779  lt2mul2div  10780  ledivmul2  10781  lemuldiv2  10783  lt2msq  10787  ltdiv23  10793  lediv23  10794  supadd  10868  supmullem1  10870  cju  10893  zextlt  11327  suprzcl  11333  zmax  11661  xrlttr  11849  xrre3  11876  qbtwnre  11904  xrsupsslem  12009  xrinfmsslem  12010  supxrunb1  12021  supxrunb2  12022  ixxdisj  12061  iooshf  12123  icodisj  12168  iccf1o  12187  modid  12557  modadd1  12569  modmul1  12585  seqf1o  12704  expsub  12770  sqlecan  12833  bcval5  12967  hashmap  13082  hashfacen  13095  seqcoll  13105  swrdswrdlem  13311  cshwidxmod  13400  2cshwcshw  13422  cshwcshid  13424  resqreu  13841  lenegsq  13908  limsupbnd2  14062  icco1  14119  rlimresb  14144  rlimsqzlem  14227  rlimsqz  14228  rlimsqz2  14229  caucvgrlem  14251  fsum0diag2  14357  o1fsum  14386  ruclem8  14805  dvdsmulcr  14849  ndvdsadd  14972  bitsshft  15035  lcmdvds  15159  hashdvds  15318  eulerthlem2  15325  phisum  15333  pcqmul  15396  pcmpt  15434  prmreclem3  15460  4sqlem11  15497  0ram  15562  ramub1  15570  invfun  16247  initoeu2lem2  16488  coaval  16541  catcisolem  16579  funcestrcsetclem8  16610  fullestrcsetc  16614  embedsetcestrclem  16620  funcsetcestrclem8  16625  fullsetcestrc  16629  prfcl  16666  prf1st  16667  prf2nd  16668  1st2ndprf  16669  curfuncf  16701  isposd  16778  lubun  16946  isacs3lem  16989  pslem  17029  psss  17037  pwsdiagmhm  17192  gsumccat  17201  grpinvid1  17293  grpinvid2  17294  grplcan  17300  grpnpncan0  17334  dfgrp3lem  17336  dfgrp3  17337  grplactcnv  17341  0nsg  17462  eqger  17467  resghm  17499  conjghm  17514  subgga  17556  gaorber  17564  gastacl  17565  orbsta  17569  symgextf1lem  17663  psgnunilem2  17738  odid  17780  odmulg  17796  gexid  17819  odcau  17842  lsmssv  17881  lsmcom2  17893  pj1ghm  17939  frgpuptf  18006  frgpup1  18011  ghmplusg  18072  cyggex2  18121  gsumval3eu  18128  gsumval3  18131  ablfac1eu  18295  pgpfac1lem5  18301  isdrngd  18595  issrngd  18684  lmhmf1o  18867  lmhmima  18868  lmhmpreima  18869  lspextmo  18877  pwssplit2  18881  pwssplit3  18882  lspdisj  18946  islbs3  18976  lbsextlem4  18982  drngnidl  19050  lidldvgen  19076  issubassa2  19166  psrbagconf1o  19195  evlslem2  19333  ply1sclf1  19480  cnsubrg  19625  znunit  19731  cygznlem3  19737  dsmmsubg  19906  dsmmlss  19907  frlmsslsp  19954  frlmup1  19956  lindfrn  19979  f1lindf  19980  mamuass  20027  dmatmul  20122  dmatsubcl  20123  dmatmulcl  20125  dmatcrng  20127  scmataddcl  20141  scmatsubcl  20142  scmatcrng  20146  mdetunilem2  20238  pm2mpf1  20423  pm2mpghm  20440  eltg2  20573  ntrss  20669  opncldf1  20698  ssnei2  20730  neindisj  20731  restopnb  20789  restntr  20796  tgcmp  21014  hauscmplem  21019  2ndc1stc  21064  2ndcdisj  21069  2ndcomap  21071  restlly  21096  lly1stc  21109  isref  21122  islocfin  21130  comppfsc  21145  txcls  21217  txdis1cn  21248  pthaus  21251  txlm  21261  qtoptop2  21312  qtopomap  21331  kqt0lem  21349  pt1hmeo  21419  ptuncnv  21420  xkocnv  21427  fbasfip  21482  fgabs  21493  fbasrn  21498  elfm2  21562  fmfnfmlem2  21569  fmfnfmlem4  21571  ptcmplem3  21668  ptcmplem4  21669  tsmsres  21757  tsmsxplem1  21766  utoptop  21848  elbl2ps  22004  elbl2  22005  blin  22036  xmeter  22048  xmetresbl  22052  stdbdxmet  22130  metrest  22139  metustexhalf  22171  dscmet  22187  nrmmetd  22189  tngngp2  22266  nmoi2  22344  icccmplem2  22434  reconnlem2  22438  metdstri  22462  metdsle  22463  metdsre  22464  metnrmlem3  22472  fsumcn  22481  icccvx  22557  bndth  22565  evth  22566  reparphti  22605  pi1blem  22647  tchcph  22844  iscfil2  22872  cfilfcls  22880  iscau4  22885  iscauf  22886  caucfil  22889  cncmet  22927  minveclem7  23014  ovoliunlem1  23077  ovolicc2lem2  23093  ovolicc2lem3  23094  ovolicc2lem4  23095  ovolicc2lem5  23096  ovolicc2  23097  voliunlem3  23127  voliun  23129  ioombl  23140  volivth  23181  ismbfd  23213  ismbf3d  23227  itg1addlem1  23265  i1fadd  23268  itg1addlem4  23272  itg2seq  23315  itg2split  23322  itg2monolem1  23323  itg2gt0  23333  ibllem  23337  itgvallem3  23358  iblposlem  23364  dvmptfsum  23542  rolle  23557  dvlip  23560  c1liplem1  23563  lhop1  23581  lhop2  23582  dvcvx  23587  dvfsumge  23589  dvfsumrlimge0  23597  dvfsumrlim  23598  dvfsum2  23601  mdegaddle  23638  mdegvscale  23639  mdegmullem  23642  ply1divex  23700  coeeulem  23784  plyco  23801  dgrlt  23826  vieta1  23871  ulmss  23955  ulmdvlem3  23960  iblulm  23965  tanord  24088  eff1olem  24098  logdivlt  24171  logccv  24209  lawcos  24346  leibpilem1  24467  xrlimcnp  24495  cxp2limlem  24502  cxp2lim  24503  cxploglim2  24505  divsqrtsumo1  24510  lgambdd  24563  ftalem2  24600  sqff1o  24708  dvdsppwf1o  24712  dvdsflf1o  24713  musum  24717  muinv  24719  fsumdvdsmul  24721  sgmmul  24726  fsumvma  24738  logfac2  24742  chpchtsum  24744  logfacrlim  24749  logexprlim  24750  dchrelbas3  24763  dchrmulcl  24774  bposlem1  24809  lgsdchr  24880  lgsquadlem1  24905  lgsquadlem2  24906  lgsquad2lem2  24910  chebbnd1lem1  24958  chpchtlim  24968  rplogsumlem2  24974  dchrmusum2  24983  dchrvmasumlem1  24984  dchrvmasum2lem  24985  dchrvmasumlem2  24987  dchrvmasumlem3  24988  dchrvmasumiflem2  24991  dchrisum0flb  24999  dchrisum0fno1  25000  rpvmasum2  25001  dchrisum0re  25002  dchrisum0lem1  25005  dchrisum0lem2a  25006  dchrisum0lem2  25007  dchrisum0lem3  25008  rplogsum  25016  mulogsum  25021  mulog2sumlem2  25024  vmalogdivsum2  25027  2vmadivsumlem  25029  selberglem2  25035  selberg3lem1  25046  selberg4lem1  25049  selberg4  25050  pntrsumo1  25054  selberg34r  25060  pntrlog2bndlem1  25066  pntrlog2bndlem2  25067  pntrlog2bndlem3  25068  pntrlog2bndlem4  25069  pntrlog2bndlem5  25070  pntrlog2bndlem6  25072  pntibndlem3  25081  pntlemp  25099  ostthlem1  25116  ostth3  25127  ercgrg  25212  ishpg  25451  axlowdimlem15  25636  axlowdimlem16  25637  axcontlem10  25653  usgrasscusgra  26011  usgra2adedgspth  26141  usgra2adedgwlk  26142  usgra2adedgwlkon  26143  wwlknext  26252  wwlkextwrd  26256  wwlknndef  26265  clwwlknndef  26301  clwlkisclwwlklem2a  26313  frgranbnb  26547  numclwlk1lem2f1  26621  grpoidinv  26746  grporcan  26756  grpoinvid1  26766  grpoinvid2  26767  grpolcan  26768  ablo4  26788  nvabs  26911  sspph  27094  minvecolem7  27123  htthlem  27158  hvadd4  27277  hvaddsub4  27319  shscli  27560  pjspansn  27820  fh1  27861  fh2  27862  cm2j  27863  chscllem2  27881  spansncvi  27895  5oalem2  27898  5oalem5  27901  5oalem6  27902  3oalem2  27906  hoadd4  28027  cnvunop  28161  bralnfn  28191  eighmorth  28207  hmops  28263  hmopm  28264  adjlnop  28329  adjmul  28335  adjadd  28336  nmopcoi  28338  kbass5  28363  kbass6  28364  hstle  28473  stlesi  28484  mdsl0  28553  mdexchi  28578  atom1d  28596  superpos  28597  cvexchlem  28611  atomli  28625  atcvatlem  28628  chirredlem2  28634  chirredlem3  28635  atcvat4i  28640  mdsymlem1  28646  mdsymlem3  28648  mdsymlem5  28650  mdsymlem6  28651  sumdmdlem  28661  sumdmdlem2  28662  cdj1i  28676  opeldifid  28794  isoun  28862  1stpreimas  28866  f1od2  28887  archirngz  29074  archiabllem1  29078  archiabllem2c  29080  rngurd  29119  indf1ofs  29415  esum2d  29482  cntmeas  29616  ddemeas  29626  carsgclctunlem1  29706  itgeq12dv  29715  eulerpartlemgc  29751  eulerpartlemb  29757  eulerpartlemgs2  29769  ballotlemfc0  29881  ballotlemfcc  29882  signstfvneq0  29975  bnj607  30240  derangenlem  30407  subfacp1lem3  30418  subfacp1lem5  30420  cvmliftmolem2  30518  cvmliftlem6  30526  cvmlift2lem5  30543  cvmlift2lem7  30545  cvmlift2lem9  30547  mppspstlem  30722  dfon2lem6  30937  sltres  31061  colinbtwnle  31395  finminlem  31482  nn0prpwlem  31487  isfne  31504  neibastop1  31524  neibastop2lem  31525  neibastop3  31527  tailfb  31542  onsuct0  31610  nndivsub  31626  knoppcnlem6  31658  knoppndvlem9  31681  knoppndvlem18  31690  knoppndvlem21  31693  bj-finsumval0  32324  rdgeqoa  32394  matunitlindflem2  32576  poimirlem4  32583  poimirlem11  32590  poimirlem12  32591  poimirlem13  32592  poimirlem25  32604  poimirlem28  32607  heicant  32614  mblfinlem2  32617  mblfinlem3  32618  mblfinlem4  32619  mbfposadd  32627  itg2addnclem3  32633  bddiblnc  32650  ftc1anclem5  32659  ftc1anclem6  32660  ftc1anclem7  32661  ftc1anc  32663  frinfm  32700  filbcmb  32705  seqpo  32713  sstotbnd2  32743  isbndx  32751  ssbnd  32757  prdsbnd  32762  ismtycnv  32771  ismtyres  32777  heiborlem3  32782  heibor  32790  ghomdiv  32861  grpokerinj  32862  isdrngo2  32927  rngohomco  32943  rngoisocnv  32950  rngoisoco  32951  crngm4  32972  crngohomfo  32975  isidlc  32984  ispridl2  33007  ispridlc  33039  prtlem16  33172  ax12eq  33244  ax12el  33245  lshpcmp  33293  omllaw3  33550  omlfh1N  33563  cvratlem  33725  cvrat3  33746  cvrat4  33747  ps-2  33782  elpaddn0  34104  paddasslem10  34133  cdleme0cp  34519  cdleme32a  34747  cdlemeg49lebilem  34845  cdleme50eq  34847  tendoeq2  35080  diaglbN  35362  diameetN  35363  diainN  35364  dvhopN  35423  djaclN  35443  djajN  35444  dihopelvalcpre  35555  dih1dimatlem  35636  dihmeetcl  35652  djhcl  35707  mapdpglem2  35980  ismrc  36282  eldioph2  36343  lzenom  36351  rexrabdioph  36376  fphpdo  36399  irrapxlem3  36406  elpell14qr2  36444  pell14qrreccl  36446  pell14qrdich  36451  pellfundglb  36467  monotoddzzfi  36525  2nn0ind  36528  jm2.21  36579  jm2.22  36580  dnnumch3  36635  dnwech  36636  fnwe2lem2  36639  hbtlem6  36718  imo72b2lem1  37493  cncmpmax  38214  disjf1  38364  eliccelioc  38594  fprodexp  38661  fprodabs2  38662  mullimc  38683  mullimcf  38690  islpcn  38706  cncfshift  38759  cncfperiod  38764  fprodcncf  38787  dvnprodlem1  38836  dvnprodlem2  38837  stoweidlem34  38927  stoweidlem48  38941  stoweidlem60  38953  fourierdlem42  39042  fourierdlem60  39059  fourierdlem61  39060  fourierdlem63  39062  fourierdlem65  39064  fourierdlem87  39086  fourierdlem97  39096  elaa2  39127  etransclem46  39173  etransc  39176  sge0iunmptlemfi  39306  isomennd  39421  ovnsslelem  39450  ovolval4lem2  39540  ovolval5lem3  39544  smflimlem3  39659  smflimlem4  39660  smflimlem6  39662  smfpimbor1lem1  39683  icceuelpart  39974  fmtnoprmfac2  40017  bgoldbtbndlem2  40222  bgoldbtbndlem3  40223  f1cofveqaeqALT  40324  cusgrfilem1  40671  crctcsh1wlkn0  41024  wwlksnextwrd  41103  clwlkclwwlklem2a  41207  srhmsubc  41868  srhmsubcALTV  41887  aacllem  42356