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

Theorem sylancom 591
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 488 . 2 ((𝜑𝜓) → 𝜓)
3 sylancom.2 . 2 ((𝜒𝜓) → 𝜃)
41, 2, 3syl2anc 587 1 ((𝜑𝜓) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399
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 210  df-an 400
This theorem is referenced by:  sofld  6015  ordin  6193  fimacnvdisj  6535  f1oexrnex  7618  wemoiso  7660  wemoiso2  7661  smorndom  7992  rdglim  8049  oaabs  8258  ssct  8585  onomeneq  8697  domfi  8727  f1vrnfibi  8797  brwdom2  9025  infdiffi  9109  cantnflem1  9140  wemapwe  9148  cnfcom3lem  9154  r1lim  9189  carduni  9398  ac5num  9451  infunsdom1  9628  cofsmo  9684  isf32lem6  9773  hsmexlem1  9841  ac6c4  9896  fnct  9952  pwfseqlem1  10073  tskuni  10198  recgt1i  11530  avgle2  11870  eluzmn  12242  rpnnen1lem1  12369  xnn0le2is012  12631  fzneuz  12987  mulmod0  13244  hasheni  13708  hashun2  13744  reccn2  14949  isershft  15016  sumeq2ii  15046  prodeq2ii  15263  demoivreALT  15550  bitsp1  15774  gcdneg  15864  eucalginv  15922  eucalg  15925  odzdvds  16126  fldivp1  16227  prmunb  16244  vdwap1  16307  setsid  16534  acsmapd  17784  intopsn  17860  cntzidss  18464  symggrp  18524  pmtrfv  18576  odmodnn0  18664  sylow2alem1  18738  telgsumfzs  19106  dprdsn  19155  dvdsrmul1  19403  dvrid  19438  znunit  20259  isphld  20347  frlmup1  20491  evl1val  20957  evl1sca  20962  pf1const  20974  mat1f1o  21087  mat1mhm  21093  matunit  21287  pm2mpmhmlem2  21428  cctop  21615  iscnp4  21872  iscncl  21878  cnntr  21884  tx2cn  22219  xkoco1cn  22266  qtopkgen  22319  hmeontr  22378  hmeores  22380  filssufilg  22520  ustuqtop1  22851  utop2nei  22860  fmucndlem  22901  cfilufg  22903  xmetres2  22972  metres2  22974  metustto  23164  metust  23169  cfilucfil  23170  dscopn  23184  nmoi  23338  iccntr  23430  cphsqrtcl2  23795  cmsss  23959  ivthlem3  24061  sca2rab  24120  ovolicc2lem3  24127  mdegleb  24669  aalioulem3  24934  ulm2  24984  ulmcn  24998  root1eq1  25348  atanlogsublem  25505  birthdaylem3  25543  logexprlim  25813  dchrisumlem3  26079  f1otrg  26669  ax5seglem1  26726  ax5seglem2  26727  ax5seglem3a  26728  ax5seglem4  26730  ax5seglem9  26735  ax5seg  26736  axbtwnid  26737  axlowdimlem17  26756  axcontlem2  26763  axcontlem4  26765  axcontlem8  26769  rusgrnumwwlks  27764  wwlksext2clwwlk  27846  grpoidinv  28295  imsmetlem  28477  ipasslem1  28618  ip2eqi  28643  hvpncan  28826  pjid  29482  hmopre  29710  eigvalcl  29748  leopnmid  29925  superpos  30141  cvp  30162  rabfodom  30278  xlt2addrd  30512  hashxpe  30559  cyc3genpmlem  30847  lmodslmd  30886  elrspunidl  31018  prmidl0  31038  locfinreflem  31197  zarcls0  31225  fmcncfil  31288  rge0scvg  31306  esumfsup  31443  esumcvg  31459  insiga  31510  ballotlemirc  31903  signstfvcl  31957  signsvfn  31966  hashf1dmrn  32469  upgracycusgr  32516  subfacp1lem6  32546  satfdmlem  32729  msubff1  32917  fv2ndcnv  33135  matunitlindf  35054  ovoliunnfl  35098  voliunnfl  35100  volsupnfl  35101  ftc1anclem5  35133  indexa  35170  sstotbnd3  35213  heiborlem6  35253  rngosn3  35361  atlatmstc  36614  atlatle  36615  glbconN  36672  intnatN  36702  lnnat  36722  atcvrj2b  36727  atexchcvrN  36735  llncvrlpln  36853  lplncvrlvol  36911  lautcvr  37387  trlatn0  37467  cdleme48fvg  37795  cdlemg33c  38003  dihcl  38565  fsuppssind  39456  elpell1qr2  39810  oddcomabszz  39882  wepwsolem  39983  mendring  40133  mendlmod  40134  hausgraph  40153  rp-isfinite5  40222  cncmpmax  41658  eliinid  41744  icccncfext  42526  dvnprodlem2  42586  stoweidlem7  42646  stoweidlem34  42673  stoweidlem35  42674  stoweidlem59  42698  stoweidlem60  42699  stoweidlem62  42701  fourierdlem34  42780  fourierdlem73  42818  fourierdlem77  42822  etransclem35  42908  smfsuplem2  43440  pgrple2abl  44764
  Copyright terms: Public domain W3C validator