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

Theorem sylancom 589
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 486 . 2 ((𝜑𝜓) → 𝜓)
3 sylancom.2 . 2 ((𝜒𝜓) → 𝜃)
41, 2, 3syl2anc 585 1 ((𝜑𝜓) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397
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 398
This theorem is referenced by:  sofld  6140  ordin  6348  fimacnvdisj  6721  f1oexrnex  7865  wemoiso  7907  wemoiso2  7908  smocdmdom  8315  rdglim  8373  oaabs  8595  ssctOLD  8997  f1oenfi  9127  f1oenfirn  9128  f1domfi  9129  domfi  9137  sdomdomtrfi  9149  php  9155  onomeneqOLD  9174  f1vrnfibi  9282  brwdom2  9510  infdiffi  9595  cantnflem1  9626  wemapwe  9634  cnfcom3lem  9640  r1lim  9709  carduni  9918  ac5num  9973  infunsdom1  10150  cofsmo  10206  isf32lem6  10295  hsmexlem1  10363  ac6c4  10418  fnct  10474  pwfseqlem1  10595  tskuni  10720  recgt1i  12053  avgle2  12395  eluzmn  12771  rpnnen1lem1  12904  xnn0le2is012  13166  fzneuz  13523  mulmod0  13783  hasheni  14249  hashun2  14284  reccn2  15480  isershft  15549  sumeq2ii  15579  prodeq2ii  15797  demoivreALT  16084  bitsp1  16312  gcdneg  16403  eucalginv  16461  eucalg  16464  odzdvds  16668  fldivp1  16770  prmunb  16787  vdwap1  16850  setsid  17081  acsmapd  18444  intopsn  18510  cntzidss  19119  symggrp  19183  pmtrfv  19235  odmodnn0  19323  sylow2alem1  19400  telgsumfzs  19767  dprdsn  19816  dvdsrmul1  20083  dvrid  20118  znunit  20973  isphld  21061  frlmup1  21207  evl1val  21698  evl1sca  21703  pf1const  21715  mat1f1o  21830  mat1mhm  21836  matunit  22030  pm2mpmhmlem2  22171  cctop  22359  iscnp4  22617  iscncl  22623  cnntr  22629  tx2cn  22964  xkoco1cn  23011  qtopkgen  23064  hmeontr  23123  hmeores  23125  filssufilg  23265  ustuqtop1  23596  utop2nei  23605  fmucndlem  23646  cfilufg  23648  xmetres2  23717  metres2  23719  metustto  23912  metust  23917  cfilucfil  23918  dscopn  23932  nmoi  24095  iccntr  24187  cphsqrtcl2  24553  cmsss  24718  ivthlem3  24820  sca2rab  24879  ovolicc2lem3  24886  mdegleb  25432  mdegmullem  25446  aalioulem3  25697  ulm2  25747  ulmcn  25761  root1eq1  26111  atanlogsublem  26268  birthdaylem3  26306  logexprlim  26576  dchrisumlem3  26842  f1otrg  27816  ax5seglem1  27880  ax5seglem2  27881  ax5seglem3a  27882  ax5seglem4  27884  ax5seglem9  27889  ax5seg  27890  axbtwnid  27891  axlowdimlem17  27910  axcontlem2  27917  axcontlem4  27919  axcontlem8  27923  rusgrnumwwlks  28922  wwlksext2clwwlk  29004  grpoidinv  29453  imsmetlem  29635  ipasslem1  29776  ip2eqi  29801  hvpncan  29984  pjid  30640  hmopre  30868  eigvalcl  30906  leopnmid  31083  superpos  31299  cvp  31320  rabfodom  31435  ecref  31628  xlt2addrd  31666  hashxpe  31712  cyc3genpmlem  32003  lmodslmd  32042  nsgqusf1olem2  32195  elrspunidl  32206  prmidl0  32226  locfinreflem  32424  zarcls0  32452  fmcncfil  32515  rge0scvg  32533  esumfsup  32672  esumcvg  32688  insiga  32739  ballotlemirc  33134  signstfvcl  33188  signsvfn  33197  hashf1dmrn  33710  upgracycusgr  33752  subfacp1lem6  33782  satfdmlem  33965  msubff1  34153  fv2ndcnv  34355  matunitlindf  36079  ovoliunnfl  36123  voliunnfl  36125  volsupnfl  36126  ftc1anclem5  36158  indexa  36195  sstotbnd3  36238  heiborlem6  36278  rngosn3  36386  atlatmstc  37784  atlatle  37785  glbconN  37842  glbconNOLD  37843  intnatN  37873  lnnat  37893  atcvrj2b  37898  atexchcvrN  37906  llncvrlpln  38024  lplncvrlvol  38082  lautcvr  38558  trlatn0  38638  cdleme48fvg  38966  cdlemg33c  39174  dihcl  39736  fsuppssind  40771  elpell1qr2  41198  oddcomabszz  41271  wepwsolem  41372  mendring  41522  mendlmod  41523  hausgraph  41542  cantnftermord  41657  cantnfub  41658  cantnf2  41662  omabs2  41668  rp-isfinite5  41796  cncmpmax  43244  eliinid  43328  icccncfext  44135  dvnprodlem2  44195  stoweidlem7  44255  stoweidlem34  44282  stoweidlem35  44283  stoweidlem59  44307  stoweidlem60  44308  stoweidlem62  44310  fourierdlem34  44389  fourierdlem73  44427  fourierdlem77  44431  etransclem35  44517  smfsuplem2  45060  pgrple2abl  46448  clddisj  46943
  Copyright terms: Public domain W3C validator