Theorem adantrr 716

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 592	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 206  df-an 396

This theorem is referenced by:  ad2antrl  727  ad2ant2r  746  ad2ant2lr  747  cases2ALT  1047  consensus  1051  3adant3  1130  3ad2antr1  1186  reusv2lem3  5395  axprlem4  5421  otsndisj  5516  otiunsndisj  5517  po2nr  5599  sotric  5613  sotrieq  5614  tz7.7  6390  fmptsnd  7173  fvtp1g  7205  f1cofveqaeqALT  7264  fsnex  7287  isocnv  7333  isores2  7336  isomin  7340  isoini  7341  f1oiso2  7355  ovmpodf  7572  offval  7689  ordsucun  7823  xp1st  8020  cnvf1olem  8110  fnse  8133  sexp2  8146  mpoxopoveq  8219  frrlem3  8288  frrlem13  8298  wfrlem3OLD  8325  oalim  8547  omlim  8548  oaass  8576  omordi  8581  omwordri  8587  odi  8594  oen0  8601  oewordri  8607  nnawordi  8636  nnmordi  8646  omabs  8666  coflton  8686  nadd4  8713  erinxp  8804  dom2lem  9007  domssl  9013  mapen  9160  ssenen  9170  ssfiALT  9193  domfi  9211  php  9229  domunfican  9339  mapfien  9426  ordtypelem6  9541  ordtypelem7  9542  card2inf  9573  inf3lem6  9651  cantnfle  9689  cantnflem1b  9704  cantnflem1  9707  wemapwe  9715  ttrclselem2  9744  rankxplim3  9899  fseqenlem2  10043  dfac5lem4  10144  dfac2b  10148  cfsuc  10275  cfflb  10277  cofsmo  10287  infpssrlem4  10324  fin4en1  10327  ssfin4  10328  fin23lem26  10343  fin23lem22  10345  fin23lem27  10346  isf34lem4  10395  isf34lem5  10396  fin1a2lem12  10429  axdc3lem2  10469  axdc4lem  10473  ttukeylem6  10532  iundom2g  10558  pwcfsdom  10601  gchen2  10644  gchor  10645  fpwwe2lem6  10654  fpwwe2lem8  10656  fpwwe2lem10  10658  fpwwe2lem11  10659  fpwwe2  10661  pwfseqlem4  10680  gchina  10717  ltexprlem6  11059  prlem936  11065  mul4  11407  2addsub  11499  muladd  11671  ltleadd  11722  leord1  11766  eqord1  11767  ltord2  11768  leord2  11769  eqord2  11770  divmul3  11902  divcan7  11948  divadddiv  11954  lemul2a  12094  lemul12b  12096  ltmuldiv2  12113  ltdivmul  12114  ledivmul  12115  ltdivmul2  12116  lt2mul2div  12117  ledivmul2  12118  lemuldiv2  12120  lt2msq  12124  ltdiv23  12130  lediv23  12131  fimaxre  12183  supadd  12207  supmullem1  12209  cju  12233  zextlt  12661  suprzcl  12667  zmax  12954  xrlttr  13146  xrre3  13177  qbtwnre  13205  xrsupsslem  13313  xrinfmsslem  13314  supxrunb1  13325  supxrunb2  13326  ixxdisj  13366  iooshf  13430  icodisj  13480  iccf1o  13500  modid  13888  modadd1  13900  modmul1  13916  seqf1o  14035  expsub  14102  sqlecan  14199  bcval5  14304  hashmap  14421  hashfacen  14440  hashfacenOLD  14441  seqcoll  14452  swrdswrdlem  14681  swrdccatin2  14706  cshwidxmod  14780  2cshwcshw  14803  cshwcshid  14805  resqreu  15226  lenegsq  15294  limsupbnd2  15454  icco1  15511  rlimresb  15536  rlimsqzlem  15622  rlimsqz  15623  rlimsqz2  15624  caucvgrlem  15646  fsum0diag2  15756  o1fsum  15786  ruclem8  16208  dvdsmulcr  16257  ndvdsadd  16381  bitsshft  16444  lcmdvds  16573  hashdvds  16738  eulerthlem2  16745  phisum  16753  pcqmul  16816  pcmpt  16855  prmreclem3  16881  4sqlem11  16918  0ram  16983  ramub1  16991  invfun  17741  initoeu2lem2  17998  coaval  18051  catcisolem  18093  funcestrcsetclem8  18132  fullestrcsetc  18136  embedsetcestrclem  18142  funcsetcestrclem8  18147  fullsetcestrc  18151  prfcl  18188  prf1st  18189  prf2nd  18190  1st2ndprf  18191  curfuncf  18224  isposd  18309  lubun  18501  isacs3lem  18528  pslem  18558  psss  18566  pwsdiagmhm  18777  grpinvid1  18942  grpinvid2  18943  grplcan  18951  grpnpncan0  18986  dfgrp3lem  18988  dfgrp3  18989  grplactcnv  18993  0nsg  19118  eqger  19127  eqg0subg  19145  qus0subgadd  19148  resghm  19180  conjghm  19197  subgga  19245  gaorber  19253  gastacl  19254  orbsta  19258  symgextf1lem  19369  psgnunilem2  19444  odid  19487  odmulg  19505  gexid  19530  odcau  19553  lsmssv  19592  lsmcom2  19604  pj1ghm  19652  frgpuptf  19719  frgpup1  19724  ghmplusg  19795  cyggex2  19846  gsumval3eu  19853  gsumval3  19856  ablfac1eu  20024  pgpfac1lem5  20030  ablsimpgfind  20061  ringurd  20119  srhmsubc  20607  isdrngd  20651  isdrngdOLD  20653  issrngd  20735  lmhmf1o  20925  lmhmima  20926  lmhmpreima  20927  lspextmo  20935  pwssplit2  20939  pwssplit3  20940  lspdisj  21007  islbs3  21037  lbsextlem4  21043  drngnidl  21132  rngqiprngghmlem2  21172  rngqiprnglinlem1  21175  rngqiprngghm  21183  lidldvgen  21218  isdomn4  21244  cnsubrg  21354  znunit  21491  cygznlem3  21497  dsmmsubg  21671  dsmmlss  21672  frlmsslsp  21724  frlmup1  21726  lindfrn  21749  f1lindf  21750  issubassa2  21819  psrbagconf1o  21864  psrbagconf1oOLD  21865  psrgrp  21893  evlslem2  22019  mhplss  22073  psdmul  22084  ply1sclf1  22202  mamuass  22296  dmatmul  22393  dmatsubcl  22394  dmatmulcl  22396  dmatcrng  22398  scmataddcl  22412  scmatsubcl  22413  scmatcrng  22417  mdetunilem2  22509  pm2mpf1  22695  pm2mpghm  22712  eltg2  22855  ntrss  22953  opncldf1  22982  ssnei2  23014  neindisj  23015  restopnb  23073  restntr  23080  tgcmp  23299  hauscmplem  23304  2ndc1stc  23349  2ndcdisj  23354  2ndcomap  23356  restlly  23381  lly1stc  23394  isref  23407  islocfin  23415  comppfsc  23430  txcls  23502  txdis1cn  23533  pthaus  23536  txlm  23546  qtoptop2  23597  qtopomap  23616  kqt0lem  23634  pt1hmeo  23704  ptuncnv  23705  xkocnv  23712  fbasfip  23766  fgabs  23777  fbasrn  23782  elfm2  23846  fmfnfmlem2  23853  fmfnfmlem4  23855  ptcmplem3  23952  ptcmplem4  23953  tsmsres  24042  tsmsxplem1  24051  utoptop  24133  elbl2ps  24289  elbl2  24290  blin  24321  xmeter  24333  xmetresbl  24337  stdbdxmet  24418  metrest  24427  metustexhalf  24459  dscmet  24475  nrmmetd  24477  tngngp2  24563  nmoi2  24641  icccmplem2  24733  reconnlem2  24737  metdstri  24761  metdsle  24762  metdsre  24763  metnrmlem3  24771  fsumcn  24782  icccvx  24869  bndth  24878  evth  24879  reparphti  24917  reparphtiOLD  24918  pi1blem  24960  tcphcph  25159  iscfil2  25188  cfilfcls  25196  iscau4  25201  iscauf  25202  caucfil  25205  cncmet  25244  minveclem7  25357  ovoliunlem1  25425  ovolicc2lem2  25441  ovolicc2lem3  25442  ovolicc2lem4  25443  ovolicc2lem5  25444  ovolicc2  25445  voliunlem3  25475  voliun  25477  ioombl  25488  volivth  25530  ismbfd  25562  ismbf3d  25577  itg1addlem1  25615  i1fadd  25618  itg1addlem4  25622  itg1addlem4OLD  25623  itg2split  25673  itg2monolem1  25674  itg2gt0  25684  ibllem  25688  itgvallem3  25709  iblposlem  25715  bddiblnc  25765  dvmptfsum  25901  rolle  25916  dvlip  25920  c1liplem1  25923  lhop1  25941  lhop2  25942  dvcvx  25947  dvfsumge  25950  dvfsumrlimge0  25959  dvfsumrlim  25960  dvfsum2  25963  mdegaddle  26004  mdegvscale  26005  mdegmullem  26008  ply1divex  26066  coeeulem  26152  plyco  26169  dgrlt  26195  vieta1  26241  ulmss  26327  ulmdvlem3  26332  iblulm  26337  tanord  26466  eff1olem  26476  logdivlt  26549  logccv  26591  lawcos  26742  xrlimcnp  26894  cxp2limlem  26902  cxp2lim  26903  cxploglim2  26905  divsqrtsumo1  26910  lgambdd  26963  sqff1o  27108  dvdsppwf1o  27112  dvdsflf1o  27113  musum  27117  muinv  27119  fsumdvdsmul  27121  fsumdvdsmulOLD  27123  sgmmul  27128  fsumvma  27140  logfac2  27144  chpchtsum  27146  logfacrlim  27151  logexprlim  27152  dchrelbas3  27165  dchrmulcl  27176  bposlem1  27211  lgsdchr  27282  lgsquadlem1  27307  lgsquadlem2  27308  lgsquad2lem2  27312  chebbnd1lem1  27396  chpchtlim  27406  rplogsumlem2  27412  dchrmusum2  27421  dchrvmasumlem1  27422  dchrvmasum2lem  27423  dchrvmasumlem2  27425  dchrvmasumlem3  27426  dchrvmasumiflem2  27429  dchrisum0flb  27437  dchrisum0fno1  27438  rpvmasum2  27439  dchrisum0re  27440  dchrisum0lem1  27443  dchrisum0lem2a  27444  dchrisum0lem2  27445  dchrisum0lem3  27446  rplogsum  27454  mulogsum  27459  mulog2sumlem2  27462  vmalogdivsum2  27465  2vmadivsumlem  27467  selberglem2  27473  selberg3lem1  27484  selberg4lem1  27487  selberg4  27488  pntrsumo1  27492  selberg34r  27498  pntrlog2bndlem1  27504  pntrlog2bndlem2  27505  pntrlog2bndlem3  27506  pntrlog2bndlem4  27507  pntrlog2bndlem5  27508  pntrlog2bndlem6  27510  pntibndlem3  27519  pntlemp  27537  ostthlem1  27554  ostth3  27565  sltres  27589  noresle  27624  nosupno  27630  nosupbday  27632  noinfno  27645  bday1s  27758  cutlt  27846  addsproplem2  27881  negsproplem2  27935  mulsuniflem  28043  mulsunif2lem  28063  precsexlem9  28107  precsexlem10  28108  precsexlem11  28109  om2noseqlt  28166  om2noseqlt2  28167  om2noseqf1o  28168  om2noseqrdg  28171  noseqrdgfn  28173  recut  28218  renegscl  28220  ercgrg  28315  oppperpex  28551  axlowdimlem15  28761  axlowdimlem16  28762  axcontlem10  28778  cusgrfilem1  29263  upgriswlk  29449  crctcshwlkn0  29626  wwlksnext  29698  wwlksnextwrd  29702  clwlkclwwlklem2a  29802  wwlksext2clwwlk  29861  grpoidinv  30312  grporcan  30322  grpoinvid1  30332  grpoinvid2  30333  grpolcan  30334  ablo4  30354  nvabs  30476  minvecolem7  30687  htthlem  30721  hvadd4  30840  hvaddsub4  30882  shscli  31121  pjspansn  31381  fh1  31422  fh2  31423  cm2j  31424  chscllem2  31442  spansncvi  31456  5oalem2  31459  5oalem5  31462  5oalem6  31463  3oalem2  31467  hoadd4  31588  cnvunop  31722  bralnfn  31752  eighmorth  31768  hmops  31824  hmopm  31825  adjlnop  31890  adjmul  31896  adjadd  31897  nmopcoi  31899  kbass5  31924  kbass6  31925  hstle  32034  stlesi  32045  mdsl0  32114  mdexchi  32139  atom1d  32157  superpos  32158  cvexchlem  32172  atomli  32186  atcvatlem  32189  chirredlem2  32195  chirredlem3  32196  atcvat4i  32201  mdsymlem1  32207  mdsymlem3  32209  mdsymlem5  32211  mdsymlem6  32212  sumdmdlem  32222  sumdmdlem2  32223  cdj1i  32237  opeldifid  32383  isoun  32476  1stpreimas  32480  f1od2  32498  ccatf1  32667  archirngz  32892  archiabllem1  32896  archiabllem2c  32898  qusxpid  33070  indf1ofs  33640  esum2d  33707  cntmeas  33840  ddemeas  33850  carsgclctunlem1  33932  itgeq12dv  33941  eulerpartlemgc  33977  eulerpartlemb  33983  eulerpartlemgs2  33995  ballotlemfc0  34107  ballotlemfcc  34108  reprss  34244  reprpmtf1o  34253  hgt750lemb  34283  bnj607  34542  derangenlem  34776  subfacp1lem3  34787  subfacp1lem5  34789  cvmliftmolem2  34887  cvmliftlem6  34895  cvmlift2lem5  34912  cvmlift2lem7  34914  cvmlift2lem9  34916  mppspstlem  35176  dfon2lem6  35379  colinbtwnle  35709  finminlem  35797  nn0prpwlem  35801  isfne  35818  neibastop1  35838  neibastop2lem  35839  neibastop3  35841  tailfb  35856  onsuct0  35920  nndivsub  35936  knoppcnlem6  35968  knoppndvlem9  35990  knoppndvlem18  35999  knoppndvlem21  36002  bj-prmoore  36589  bj-finsumval0  36759  rdgeqoa  36844  pibt2  36891  lindsadd  37081  matunitlindflem2  37085  poimirlem4  37092  poimirlem11  37099  poimirlem12  37100  poimirlem13  37101  poimirlem25  37113  poimirlem28  37116  heicant  37123  mblfinlem2  37126  mblfinlem3  37127  mblfinlem4  37128  mbfposadd  37135  itg2addnclem3  37141  ftc1anclem5  37165  ftc1anclem6  37166  ftc1anclem7  37167  ftc1anc  37169  frinfm  37203  filbcmb  37208  seqpo  37215  sstotbnd2  37242  isbndx  37250  ssbnd  37256  prdsbnd  37261  ismtycnv  37270  ismtyres  37276  heiborlem3  37281  heibor  37289  ghomdiv  37360  grpokerinj  37361  isdrngo2  37426  rngohomco  37442  rngoisocnv  37449  rngoisoco  37450  crngm4  37471  crngohomfo  37474  isidlc  37483  ispridl2  37506  ispridlc  37538  prtlem16  38336  ax12eq  38408  ax12el  38409  lshpcmp  38455  omllaw3  38712  omlfh1N  38725  cvratlem  38889  cvrat3  38910  cvrat4  38911  ps-2  38946  elpaddn0  39268  paddasslem10  39297  cdleme0cp  39682  cdleme32a  39909  cdlemeg49lebilem  40007  cdleme50eq  40009  tendoeq2  40242  diaglbN  40523  diameetN  40524  diainN  40525  dvhopN  40584  djaclN  40604  djajN  40605  dihopelvalcpre  40716  dih1dimatlem  40797  dihmeetcl  40813  djhcl  40868  mapdpglem2  41141  3factsumint1  41487  sticksstones22  41635  metakunt2  41649  imacrhmcl  41742  frlmsnic  41761  psrmnd  41766  evlselvlem  41810  fsuppind  41814  0prjspn  42043  infdesc  42058  ismrc  42112  eldioph2  42173  lzenom  42181  rexrabdioph  42205  fphpdo  42228  irrapxlem3  42235  elpell14qr2  42273  pell14qrreccl  42275  pell14qrdich  42280  pellfundglb  42296  monotoddzzfi  42354  2nn0ind  42357  jm2.21  42406  jm2.22  42407  dnnumch3  42462  dnwech  42463  fnwe2lem2  42466  hbtlem6  42544  cantnfresb  42744  imo72b2lem1  43590  mnuprdlem1  43700  mnuprdlem2  43701  cncmpmax  44385  disjf1  44547  eliccelioc  44897  fprodexp  44973  fprodabs2  44974  mullimc  44995  mullimcf  45002  islpcn  45018  limsuppnfdlem  45080  liminfval2  45147  xlimmnfvlem1  45211  xlimmnfvlem2  45212  xlimpnfvlem1  45215  xlimpnfvlem2  45216  cncfshift  45253  cncfperiod  45258  fprodcncf  45279  dvnprodlem1  45325  dvnprodlem2  45326  stoweidlem34  45413  stoweidlem48  45427  stoweidlem60  45439  fourierdlem42  45528  fourierdlem60  45545  fourierdlem61  45546  fourierdlem63  45548  fourierdlem65  45550  fourierdlem87  45572  fourierdlem97  45582  elaa2  45613  etransclem46  45659  etransc  45662  salrestss  45740  sge0iunmptlemfi  45792  isomennd  45910  ovnsslelem  45939  ovolval4lem2  46029  smflimlem3  46152  smflimlem4  46153  smflimlem6  46155  smfpimbor1lem1  46177  smflimmpt  46189  smflimsupmpt  46208  smfliminfmpt  46211  fsetsnf1  46425  fcoresf1  46442  fvelsetpreimafv  46718  icceuelpart  46767  prproropf1olem4  46837  fmtnoprmfac2  46898  bgoldbtbndlem2  47137  bgoldbtbndlem3  47138  srhmsubcALTV  47378  catprs  48008  prsthinc  48051  aacllem  48225

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »