MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sylancom Structured version   Visualization version   GIF version

Theorem sylancom 588
Description: Syllogism inference with commutation of antecedents. (Contributed by NM, 2-Jul-2008.)
Hypotheses
Ref Expression
sylancom.1 ((𝜑𝜓) → 𝜒)
sylancom.2 ((𝜒𝜓) → 𝜃)
Assertion
Ref Expression
sylancom ((𝜑𝜓) → 𝜃)

Proof of Theorem sylancom
StepHypRef Expression
1 sylancom.1 . 2 ((𝜑𝜓) → 𝜒)
2 simpr 485 . 2 ((𝜑𝜓) → 𝜓)
3 sylancom.2 . 2 ((𝜒𝜓) → 𝜃)
41, 2, 3syl2anc 584 1 ((𝜑𝜓) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  sofld  6038  ordin  6215  fimacnvdisj  6551  f1oexrnex  7620  wemoiso  7665  wemoiso2  7666  smorndom  7996  rdglim  8053  oaabs  8261  ssct  8587  onomeneq  8697  domfi  8728  f1vrnfibi  8798  brwdom2  9026  infdiffi  9110  cantnflem1  9141  wemapwe  9149  cnfcom3lem  9155  r1lim  9190  carduni  9399  ac5num  9451  infunsdom1  9624  cofsmo  9680  isf32lem6  9769  hsmexlem1  9837  ac6c4  9892  fnct  9948  pwfseqlem1  10069  tskuni  10194  recgt1i  11526  avgle2  11867  eluzmn  12239  rpnnen1lem1  12367  xnn0le2is012  12629  fzneuz  12978  mulmod0  13235  hasheni  13698  hashun2  13734  reccn2  14943  isershft  15010  sumeq2ii  15040  prodeq2ii  15257  demoivreALT  15544  bitsp1  15770  gcdneg  15860  eucalginv  15918  eucalg  15921  odzdvds  16122  fldivp1  16223  prmunb  16240  vdwap1  16303  setsid  16528  acsmapd  17778  intopsn  17854  cntzidss  18408  symggrp  18460  pmtrfv  18511  odmodnn0  18599  sylow2alem1  18673  telgsumfzs  19040  dprdsn  19089  dvdsrmul1  19334  dvrid  19369  evl1val  20422  evl1sca  20427  pf1const  20439  znunit  20640  isphld  20728  frlmup1  20872  mat1f1o  21017  mat1mhm  21023  matunit  21217  pm2mpmhmlem2  21357  cctop  21544  iscnp4  21801  iscncl  21807  cnntr  21813  tx2cn  22148  xkoco1cn  22195  qtopkgen  22248  hmeontr  22307  hmeores  22309  filssufilg  22449  ustuqtop1  22779  utop2nei  22788  fmucndlem  22829  cfilufg  22831  xmetres2  22900  metres2  22902  metustto  23092  metust  23097  cfilucfil  23098  dscopn  23112  nmoi  23266  iccntr  23358  cphsqrtcl2  23719  cmsss  23883  ivthlem3  23983  sca2rab  24042  ovolicc2lem3  24049  mdegleb  24587  aalioulem3  24852  ulm2  24902  ulmcn  24916  root1eq1  25263  atanlogsublem  25420  birthdaylem3  25459  logexprlim  25729  dchrisumlem3  25995  f1otrg  26585  ax5seglem1  26642  ax5seglem2  26643  ax5seglem3a  26644  ax5seglem4  26646  ax5seglem9  26651  ax5seg  26652  axbtwnid  26653  axlowdimlem17  26672  axcontlem2  26679  axcontlem4  26681  axcontlem8  26685  rusgrnumwwlks  27681  wwlksext2clwwlk  27764  grpoidinv  28213  imsmetlem  28395  ipasslem1  28536  ip2eqi  28561  hvpncan  28744  pjid  29400  hmopre  29628  eigvalcl  29666  leopnmid  29843  superpos  30059  cvp  30080  rabfodom  30194  xlt2addrd  30409  hashxpe  30456  cyc3genpmlem  30721  lmodslmd  30760  locfinreflem  31004  fmcncfil  31074  rge0scvg  31092  esumfsup  31229  esumcvg  31245  insiga  31296  ballotlemirc  31689  signstfvcl  31743  signsvfn  31752  hashf1dmrn  32253  upgracycusgr  32300  subfacp1lem6  32330  satfdmlem  32513  msubff1  32701  fv2ndcnv  32919  matunitlindf  34772  ovoliunnfl  34816  voliunnfl  34818  volsupnfl  34819  ftc1anclem5  34853  indexa  34891  sstotbnd3  34937  heiborlem6  34977  rngosn3  35085  atlatmstc  36337  atlatle  36338  glbconN  36395  intnatN  36425  lnnat  36445  atcvrj2b  36450  atexchcvrN  36458  llncvrlpln  36576  lplncvrlvol  36634  lautcvr  37110  trlatn0  37190  cdleme48fvg  37518  cdlemg33c  37726  dihcl  38288  elpell1qr2  39349  oddcomabszz  39421  wepwsolem  39522  mendring  39672  mendlmod  39673  hausgraph  39692  rp-isfinite5  39763  cncmpmax  41169  eliinid  41258  icccncfext  42050  dvnprodlem2  42112  stoweidlem7  42173  stoweidlem34  42200  stoweidlem35  42201  stoweidlem59  42225  stoweidlem60  42226  stoweidlem62  42228  fourierdlem34  42307  fourierdlem73  42345  fourierdlem77  42349  etransclem35  42435  smfsuplem2  42967  pgrple2abl  44311
  Copyright terms: Public domain W3C validator