Theorem adantrr 753

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

Syntax hints:   → wi 4   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  ad2ant2r  783  ad2ant2lr  784  cases2  993  consensus  999  3ad2antr1  1226  reusv2lem3  4871  otsndisj  4979  otiunsndisj  4980  po2nr  5048  sotric  5061  sotrieq  5062  tz7.7  5749  fmptsnd  6435  fvtp1g  6463  f1cofveqaeqALT  6516  fsnex  6538  isocnv  6580  isores2  6583  isomin  6587  isoini  6588  f1oiso2  6602  ovmpt2df  6792  offval  6904  ordsucun  7025  xp1st  7198  1stconst  7265  cnvf1olem  7275  fnse  7294  mpt2xopoveq  7345  wfrlem3  7416  oalim  7612  omlim  7613  oaass  7641  omordi  7646  omwordri  7652  odi  7659  oen0  7666  oewordri  7672  nnawordi  7701  nnmordi  7711  omabs  7727  erinxp  7821  dom2lem  7995  mapen  8124  ssenen  8134  ssfi  8180  domfi  8181  domunfican  8233  mapfien  8313  ordtypelem6  8428  ordtypelem7  8429  card2inf  8460  inf3lem6  8530  cantnfle  8568  cantnflem1b  8583  cantnflem1  8586  wemapwe  8594  rankxplim3  8744  fseqenlem2  8848  dfac5lem4  8949  dfac2  8953  cfsuc  9079  cfflb  9081  cofsmo  9091  infpssrlem4  9128  fin4en1  9131  ssfin4  9132  fin23lem26  9147  fin23lem22  9149  fin23lem27  9150  isf34lem4  9199  isf34lem5  9200  fin1a2lem12  9233  axdc3lem2  9273  axdc4lem  9277  ttukeylem6  9336  iundom2g  9362  pwcfsdom  9405  gchen2  9448  gchor  9449  fpwwe2lem7  9458  fpwwe2lem9  9460  fpwwe2lem11  9462  fpwwe2lem12  9463  fpwwe2  9465  pwfseqlem4  9484  gchina  9521  ltexprlem6  9863  prlem936  9869  mul4  10205  2addsub  10295  muladd  10462  ltleadd  10511  leord1  10555  eqord1  10556  ltord2  10557  leord2  10558  eqord2  10559  divmul3  10690  divcan7  10734  divadddiv  10740  lemul2a  10878  lemul12b  10880  ltmuldiv2  10897  ltdivmul  10898  ledivmul  10899  ltdivmul2  10900  lt2mul2div  10901  ledivmul2  10902  lemuldiv2  10904  lt2msq  10908  ltdiv23  10914  lediv23  10915  supadd  10991  supmullem1  10993  cju  11016  zextlt  11451  suprzcl  11457  zmax  11785  xrlttr  11973  xrre3  12002  qbtwnre  12030  xrsupsslem  12137  xrinfmsslem  12138  supxrunb1  12149  supxrunb2  12150  ixxdisj  12190  iooshf  12252  icodisj  12297  iccf1o  12316  modid  12695  modadd1  12707  modmul1  12723  seqf1o  12842  expsub  12908  sqlecan  12971  bcval5  13105  hashmap  13222  hashfacen  13238  seqcoll  13248  swrdswrdlem  13459  cshwidxmod  13549  2cshwcshw  13571  cshwcshid  13573  resqreu  13993  lenegsq  14060  limsupbnd2  14214  icco1  14271  rlimresb  14296  rlimsqzlem  14379  rlimsqz  14380  rlimsqz2  14381  caucvgrlem  14403  fsum0diag2  14515  o1fsum  14545  ruclem8  14966  dvdsmulcr  15011  ndvdsadd  15134  bitsshft  15197  lcmdvds  15321  hashdvds  15480  eulerthlem2  15487  phisum  15495  pcqmul  15558  pcmpt  15596  prmreclem3  15622  4sqlem11  15659  0ram  15724  ramub1  15732  invfun  16424  initoeu2lem2  16665  coaval  16718  catcisolem  16756  funcestrcsetclem8  16787  fullestrcsetc  16791  embedsetcestrclem  16797  funcsetcestrclem8  16802  fullsetcestrc  16806  prfcl  16843  prf1st  16844  prf2nd  16845  1st2ndprf  16846  curfuncf  16878  isposd  16955  lubun  17123  isacs3lem  17166  pslem  17206  psss  17214  pwsdiagmhm  17369  gsumccat  17378  grpinvid1  17470  grpinvid2  17471  grplcan  17477  grpnpncan0  17511  dfgrp3lem  17513  dfgrp3  17514  grplactcnv  17518  0nsg  17639  eqger  17644  resghm  17676  conjghm  17691  subgga  17733  gaorber  17741  gastacl  17742  orbsta  17746  symgextf1lem  17840  psgnunilem2  17915  odid  17957  odmulg  17973  gexid  17996  odcau  18019  lsmssv  18058  lsmcom2  18070  pj1ghm  18116  frgpuptf  18183  frgpup1  18188  ghmplusg  18249  cyggex2  18298  gsumval3eu  18305  gsumval3  18308  ablfac1eu  18472  pgpfac1lem5  18478  isdrngd  18772  issrngd  18861  lmhmf1o  19046  lmhmima  19047  lmhmpreima  19048  lspextmo  19056  pwssplit2  19060  pwssplit3  19061  lspdisj  19125  islbs3  19155  lbsextlem4  19161  drngnidl  19229  lidldvgen  19255  issubassa2  19345  psrbagconf1o  19374  evlslem2  19512  ply1sclf1  19659  cnsubrg  19806  znunit  19912  cygznlem3  19918  dsmmsubg  20087  dsmmlss  20088  frlmsslsp  20135  frlmup1  20137  lindfrn  20160  f1lindf  20161  mamuass  20208  dmatmul  20303  dmatsubcl  20304  dmatmulcl  20306  dmatcrng  20308  scmataddcl  20322  scmatsubcl  20323  scmatcrng  20327  mdetunilem2  20419  pm2mpf1  20604  pm2mpghm  20621  eltg2  20762  ntrss  20859  opncldf1  20888  ssnei2  20920  neindisj  20921  restopnb  20979  restntr  20986  tgcmp  21204  hauscmplem  21209  2ndc1stc  21254  2ndcdisj  21259  2ndcomap  21261  restlly  21286  lly1stc  21299  isref  21312  islocfin  21320  comppfsc  21335  txcls  21407  txdis1cn  21438  pthaus  21441  txlm  21451  qtoptop2  21502  qtopomap  21521  kqt0lem  21539  pt1hmeo  21609  ptuncnv  21610  xkocnv  21617  fbasfip  21672  fgabs  21683  fbasrn  21688  elfm2  21752  fmfnfmlem2  21759  fmfnfmlem4  21761  ptcmplem3  21858  ptcmplem4  21859  tsmsres  21947  tsmsxplem1  21956  utoptop  22038  elbl2ps  22194  elbl2  22195  blin  22226  xmeter  22238  xmetresbl  22242  stdbdxmet  22320  metrest  22329  metustexhalf  22361  dscmet  22377  nrmmetd  22379  tngngp2  22456  nmoi2  22534  icccmplem2  22626  reconnlem2  22630  metdstri  22654  metdsle  22655  metdsre  22656  metnrmlem3  22664  fsumcn  22673  icccvx  22749  bndth  22757  evth  22758  reparphti  22797  pi1blem  22839  tchcph  23036  iscfil2  23064  cfilfcls  23072  iscau4  23077  iscauf  23078  caucfil  23081  cncmet  23119  minveclem7  23206  ovoliunlem1  23270  ovolicc2lem2  23286  ovolicc2lem3  23287  ovolicc2lem4  23288  ovolicc2lem5  23289  ovolicc2  23290  voliunlem3  23320  voliun  23322  ioombl  23333  volivth  23375  ismbfd  23407  ismbf3d  23421  itg1addlem1  23459  i1fadd  23462  itg1addlem4  23466  itg2seq  23509  itg2split  23516  itg2monolem1  23517  itg2gt0  23527  ibllem  23531  itgvallem3  23552  iblposlem  23558  dvmptfsum  23738  rolle  23753  dvlip  23756  c1liplem1  23759  lhop1  23777  lhop2  23778  dvcvx  23783  dvfsumge  23785  dvfsumrlimge0  23793  dvfsumrlim  23794  dvfsum2  23797  mdegaddle  23834  mdegvscale  23835  mdegmullem  23838  ply1divex  23896  coeeulem  23980  plyco  23997  dgrlt  24022  vieta1  24067  ulmss  24151  ulmdvlem3  24156  iblulm  24161  tanord  24284  eff1olem  24294  logdivlt  24367  logccv  24409  lawcos  24546  leibpilem1  24667  xrlimcnp  24695  cxp2limlem  24702  cxp2lim  24703  cxploglim2  24705  divsqrtsumo1  24710  lgambdd  24763  ftalem2  24800  sqff1o  24908  dvdsppwf1o  24912  dvdsflf1o  24913  musum  24917  muinv  24919  fsumdvdsmul  24921  sgmmul  24926  fsumvma  24938  logfac2  24942  chpchtsum  24944  logfacrlim  24949  logexprlim  24950  dchrelbas3  24963  dchrmulcl  24974  bposlem1  25009  lgsdchr  25080  lgsquadlem1  25105  lgsquadlem2  25106  lgsquad2lem2  25110  chebbnd1lem1  25158  chpchtlim  25168  rplogsumlem2  25174  dchrmusum2  25183  dchrvmasumlem1  25184  dchrvmasum2lem  25185  dchrvmasumlem2  25187  dchrvmasumlem3  25188  dchrvmasumiflem2  25191  dchrisum0flb  25199  dchrisum0fno1  25200  rpvmasum2  25201  dchrisum0re  25202  dchrisum0lem1  25205  dchrisum0lem2a  25206  dchrisum0lem2  25207  dchrisum0lem3  25208  rplogsum  25216  mulogsum  25221  mulog2sumlem2  25224  vmalogdivsum2  25227  2vmadivsumlem  25229  selberglem2  25235  selberg3lem1  25246  selberg4lem1  25249  selberg4  25250  pntrsumo1  25254  selberg34r  25260  pntrlog2bndlem1  25266  pntrlog2bndlem2  25267  pntrlog2bndlem3  25268  pntrlog2bndlem4  25269  pntrlog2bndlem5  25270  pntrlog2bndlem6  25272  pntibndlem3  25281  pntlemp  25299  ostthlem1  25316  ostth3  25327  ercgrg  25412  ishpg  25651  axlowdimlem15  25836  axlowdimlem16  25837  axcontlem10  25853  cusgrfilem1  26351  upgriswlk  26537  crctcshwlkn0  26713  wwlksnextwrd  26792  clwlkclwwlklem2a  26899  grpoidinv  27362  grporcan  27372  grpoinvid1  27382  grpoinvid2  27383  grpolcan  27384  ablo4  27404  nvabs  27527  sspph  27710  minvecolem7  27739  htthlem  27774  hvadd4  27893  hvaddsub4  27935  shscli  28176  pjspansn  28436  fh1  28477  fh2  28478  cm2j  28479  chscllem2  28497  spansncvi  28511  5oalem2  28514  5oalem5  28517  5oalem6  28518  3oalem2  28522  hoadd4  28643  cnvunop  28777  bralnfn  28807  eighmorth  28823  hmops  28879  hmopm  28880  adjlnop  28945  adjmul  28951  adjadd  28952  nmopcoi  28954  kbass5  28979  kbass6  28980  hstle  29089  stlesi  29100  mdsl0  29169  mdexchi  29194  atom1d  29212  superpos  29213  cvexchlem  29227  atomli  29241  atcvatlem  29244  chirredlem2  29250  chirredlem3  29251  atcvat4i  29256  mdsymlem1  29262  mdsymlem3  29264  mdsymlem5  29266  mdsymlem6  29267  sumdmdlem  29277  sumdmdlem2  29278  cdj1i  29292  opeldifid  29412  isoun  29479  1stpreimas  29483  f1od2  29499  archirngz  29743  archiabllem1  29747  archiabllem2c  29749  rngurd  29788  indf1ofs  30088  esum2d  30155  cntmeas  30289  ddemeas  30299  carsgclctunlem1  30379  itgeq12dv  30388  eulerpartlemgc  30424  eulerpartlemb  30430  eulerpartlemgs2  30442  ballotlemfc0  30554  ballotlemfcc  30555  signstfvneq0  30649  reprss  30695  reprpmtf1o  30704  hgt750lemb  30734  bnj607  30986  derangenlem  31153  subfacp1lem3  31164  subfacp1lem5  31166  cvmliftmolem2  31264  cvmliftlem6  31272  cvmlift2lem5  31289  cvmlift2lem7  31291  cvmlift2lem9  31293  mppspstlem  31468  dfon2lem6  31693  sltres  31815  noresle  31846  nosupno  31849  colinbtwnle  32225  finminlem  32312  nn0prpwlem  32317  isfne  32334  neibastop1  32354  neibastop2lem  32355  neibastop3  32357  tailfb  32372  onsuct0  32440  nndivsub  32456  knoppcnlem6  32488  knoppndvlem9  32511  knoppndvlem18  32520  knoppndvlem21  32523  bj-finsumval0  33147  rdgeqoa  33218  matunitlindflem2  33406  poimirlem4  33413  poimirlem11  33420  poimirlem12  33421  poimirlem13  33422  poimirlem25  33434  poimirlem28  33437  heicant  33444  mblfinlem2  33447  mblfinlem3  33448  mblfinlem4  33449  mbfposadd  33457  itg2addnclem3  33463  bddiblnc  33480  ftc1anclem5  33489  ftc1anclem6  33490  ftc1anclem7  33491  ftc1anc  33493  frinfm  33530  filbcmb  33535  seqpo  33543  sstotbnd2  33573  isbndx  33581  ssbnd  33587  prdsbnd  33592  ismtycnv  33601  ismtyres  33607  heiborlem3  33612  heibor  33620  ghomdiv  33691  grpokerinj  33692  isdrngo2  33757  rngohomco  33773  rngoisocnv  33780  rngoisoco  33781  crngm4  33802  crngohomfo  33805  isidlc  33814  ispridl2  33837  ispridlc  33869  prtlem16  34154  ax12eq  34226  ax12el  34227  lshpcmp  34275  omllaw3  34532  omlfh1N  34545  cvratlem  34707  cvrat3  34728  cvrat4  34729  ps-2  34764  elpaddn0  35086  paddasslem10  35115  cdleme0cp  35501  cdleme32a  35729  cdlemeg49lebilem  35827  cdleme50eq  35829  tendoeq2  36062  diaglbN  36344  diameetN  36345  diainN  36346  dvhopN  36405  djaclN  36425  djajN  36426  dihopelvalcpre  36537  dih1dimatlem  36618  dihmeetcl  36634  djhcl  36689  mapdpglem2  36962  ismrc  37264  eldioph2  37325  lzenom  37333  rexrabdioph  37358  fphpdo  37381  irrapxlem3  37388  elpell14qr2  37426  pell14qrreccl  37428  pell14qrdich  37433  pellfundglb  37449  monotoddzzfi  37507  2nn0ind  37510  jm2.21  37561  jm2.22  37562  dnnumch3  37617  dnwech  37618  fnwe2lem2  37621  hbtlem6  37699  imo72b2lem1  38471  cncmpmax  39191  disjf1  39369  eliccelioc  39747  fprodexp  39826  fprodabs2  39827  mullimc  39848  mullimcf  39855  islpcn  39871  limsuppnfdlem  39933  liminfval2  40000  xlimmnfvlem1  40058  xlimmnfvlem2  40059  xlimpnfvlem1  40062  xlimpnfvlem2  40063  cncfshift  40087  cncfperiod  40092  fprodcncf  40114  dvnprodlem1  40161  dvnprodlem2  40162  stoweidlem34  40251  stoweidlem48  40265  stoweidlem60  40277  fourierdlem42  40366  fourierdlem60  40383  fourierdlem61  40384  fourierdlem63  40386  fourierdlem65  40388  fourierdlem87  40410  fourierdlem97  40420  elaa2  40451  etransclem46  40497  etransc  40500  sge0iunmptlemfi  40630  isomennd  40745  ovnsslelem  40774  ovolval4lem2  40864  ovolval5lem3  40868  smflimlem3  40981  smflimlem4  40982  smflimlem6  40984  smfpimbor1lem1  41005  smflimmpt  41016  smflimsupmpt  41035  smfliminfmpt  41038  icceuelpart  41372  fmtnoprmfac2  41479  bgoldbtbndlem2  41694  bgoldbtbndlem3  41695  srhmsubc  42076  srhmsubcALTV  42094  aacllem  42547