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

Theorem sylancom 704
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 479 . 2 ((𝜑𝜓) → 𝜓)
3 sylancom.2 . 2 ((𝜒𝜓) → 𝜃)
41, 2, 3syl2anc 696 1 ((𝜑𝜓) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 385
This theorem is referenced by:  adant423OLD  858  sofld  5735  ordin  5910  fimacnvdisj  6240  f1oexrnex  7276  wemoiso  7314  wemoiso2  7315  smorndom  7630  rdglim  7687  oaabs  7889  ssct  8202  onomeneq  8311  domfi  8342  f1vrnfibi  8412  brwdom2  8639  infdiffi  8724  cantnflem1  8755  wemapwe  8763  cnfcom3lem  8769  r1lim  8804  carduni  8993  ac5num  9045  infunsdom1  9223  cofsmo  9279  isf32lem6  9368  hsmexlem1  9436  ac6c4  9491  fnct  9547  pwfseqlem1  9668  tskuni  9793  recgt1i  11108  avgle2  11461  eluzmn  11882  rpnnen1lem1  12004  rpnnen1lem1OLD  12010  xnn0le2is012  12265  ioodisj  12491  fzneuz  12610  mulmod0  12866  hasheni  13326  hashun2  13360  swrdccatin1  13679  reccn2  14522  isershft  14589  sumeq2ii  14618  prodeq2ii  14838  demoivreALT  15126  bitsp1  15351  gcdneg  15441  eucalginv  15495  eucalg  15498  odzdvds  15698  fldivp1  15799  prmunb  15816  vdwap1  15879  setsid  16112  funcsetcestrclem7  16998  acsmapd  17375  intopsn  17450  cntzidss  17966  symggrp  18016  odmodnn0  18155  sylow2alem1  18228  telgsumfzs  18582  dprdsn  18631  dvdsrmul1  18849  dvrid  18884  evl1val  19891  evl1sca  19896  pf1const  19908  znunit  20110  isphld  20197  frlmup1  20335  mat1f1o  20482  mat1mhm  20488  matunit  20682  pm2mpmhmlem2  20822  cctop  21008  iscnp4  21265  iscncl  21271  cnntr  21277  tx2cn  21611  xkoco1cn  21658  qtopkgen  21711  hmeontr  21770  hmeores  21772  filssufilg  21912  ustuqtop1  22242  ustuqtop2  22243  utop2nei  22251  fmucndlem  22292  cfilufg  22294  xmetres2  22363  metres2  22365  metustto  22555  cfilucfil  22561  dscopn  22575  nmoi  22729  iccntr  22821  cphsqrtcl2  23182  cmsss  23343  ivthlem3  23418  sca2rab  23476  ovolicc2lem3  23483  mdegleb  24019  aalioulem3  24284  ulm2  24334  ulmcn  24348  root1eq1  24691  atanlogsublem  24837  birthdaylem3  24875  logexprlim  25145  dchrisumlem3  25375  tglowdim1i  25591  f1otrg  25946  f1otrge  25947  ax5seglem1  26003  ax5seglem2  26004  ax5seglem3a  26005  ax5seglem4  26007  ax5seglem9  26012  ax5seg  26013  axbtwnid  26014  axlowdimlem17  26033  axcontlem2  26040  axcontlem4  26042  axcontlem8  26046  rusgrnumwwlks  27092  grpoidinv  27667  imsmetlem  27850  ipasslem1  27991  ip2eqi  28017  hvpncan  28201  pjid  28859  hmopre  29087  eigvalcl  29125  leopnmid  29302  superpos  29518  cvp  29539  rabfodom  29647  xlt2addrd  29828  lmodslmd  30062  locfinreflem  30212  prsdm  30265  prsrn  30266  fmcncfil  30282  rge0scvg  30300  esumfsup  30437  esumcvg  30453  insiga  30505  ballotlemirc  30898  signstfvcl  30955  subfacp1lem6  31470  msubff1  31756  fv2ndcnv  31982  matunitlindf  33716  ovoliunnfl  33760  voliunnfl  33762  volsupnfl  33763  ftc1anclem5  33798  indexa  33837  sstotbnd3  33884  heiborlem6  33924  rngosn3  34032  atlatmstc  35105  atlatle  35106  glbconN  35162  intnatN  35192  lnnat  35212  atcvrj2b  35217  atexchcvrN  35225  llncvrlpln  35343  lplncvrlvol  35401  lautcvr  35877  trlatn0  35958  cdleme48fvg  36286  cdlemg33c  36494  dihcl  37057  elpell1qr2  37934  oddcomabszz  38007  wepwsolem  38110  mendring  38260  mendlmod  38261  hausgraph  38288  rp-isfinite5  38361  cncmpmax  39686  eliinid  39789  icccncfext  40599  dvnprodlem2  40661  stoweidlem7  40723  stoweidlem34  40750  stoweidlem35  40751  stoweidlem59  40775  stoweidlem60  40776  stoweidlem62  40778  fourierdlem34  40857  fourierdlem73  40895  fourierdlem77  40899  etransclem35  40985  smfsuplem2  41520  pgrple2abl  42652
  Copyright terms: Public domain W3C validator