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

Theorem sylancom 702
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 476 . 2 ((𝜑𝜓) → 𝜓)
3 sylancom.2 . 2 ((𝜒𝜓) → 𝜃)
41, 2, 3syl2anc 694 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  840  sofld  5616  ordin  5791  fimacnvdisj  6121  f1oexrnex  7157  wemoiso  7195  wemoiso2  7196  smorndom  7510  rdglim  7567  oaabs  7769  ssct  8082  onomeneq  8191  domfi  8222  f1vrnfibi  8292  brwdom2  8519  infdiffi  8593  cantnflem1  8624  wemapwe  8632  cnfcom3lem  8638  r1lim  8673  carduni  8845  ac5num  8897  infunsdom1  9073  cofsmo  9129  isf32lem6  9218  hsmexlem1  9286  ac6c4  9341  fnct  9397  pwfseqlem1  9518  tskuni  9643  recgt1i  10958  avgle2  11311  eluzmn  11732  rpnnen1lem1  11853  rpnnen1lem1OLD  11859  xnn0le2is012  12114  ioodisj  12340  fzneuz  12459  mulmod0  12716  hasheni  13176  hashun2  13210  swrdccatin1  13529  reccn2  14371  isershft  14438  sumeq2ii  14467  prodeq2ii  14687  demoivreALT  14975  bitsp1  15200  gcdneg  15290  eucalginv  15344  eucalg  15347  odzdvds  15547  fldivp1  15648  prmunb  15665  vdwap1  15728  setsid  15961  funcsetcestrclem7  16848  acsmapd  17225  intopsn  17300  cntzidss  17816  symggrp  17866  odmodnn0  18005  sylow2alem1  18078  telgsumfzs  18432  dprdsn  18481  dvdsrmul1  18699  dvrid  18734  evl1val  19741  evl1sca  19746  pf1const  19758  znunit  19960  isphld  20047  frlmup1  20185  mat1f1o  20332  mat1mhm  20338  matunit  20532  pm2mpmhmlem2  20672  cctop  20858  iscnp4  21115  iscncl  21121  cnntr  21127  tx2cn  21461  xkoco1cn  21508  qtopkgen  21561  hmeontr  21620  hmeores  21622  filssufilg  21762  ustuqtop1  22092  ustuqtop2  22093  utop2nei  22101  fmucndlem  22142  cfilufg  22144  xmetres2  22213  metres2  22215  metustto  22405  cfilucfil  22411  dscopn  22425  nmoi  22579  iccntr  22671  cphsqrtcl2  23032  cmsss  23193  ivthlem3  23268  sca2rab  23326  ovolicc2lem3  23333  mdegleb  23869  aalioulem3  24134  ulm2  24184  ulmcn  24198  root1eq1  24541  atanlogsublem  24687  birthdaylem3  24725  logexprlim  24995  dchrisumlem3  25225  tglowdim1i  25441  f1otrg  25796  f1otrge  25797  ax5seglem1  25853  ax5seglem2  25854  ax5seglem3a  25855  ax5seglem4  25857  ax5seglem9  25862  ax5seg  25863  axbtwnid  25864  axlowdimlem17  25883  axcontlem2  25890  axcontlem4  25892  axcontlem8  25896  rusgrnumwwlks  26941  grpoidinv  27490  imsmetlem  27673  ipasslem1  27814  ip2eqi  27840  hvpncan  28024  pjid  28682  hmopre  28910  eigvalcl  28948  leopnmid  29125  superpos  29341  cvp  29362  rabfodom  29470  xlt2addrd  29651  lmodslmd  29885  locfinreflem  30035  prsdm  30088  prsrn  30089  fmcncfil  30105  rge0scvg  30123  esumfsup  30260  esumcvg  30276  insiga  30328  ballotlemirc  30721  signstfvcl  30778  subfacp1lem6  31293  msubff1  31579  fv2ndcnv  31805  matunitlindf  33537  ovoliunnfl  33581  voliunnfl  33583  volsupnfl  33584  ftc1anclem5  33619  indexa  33658  sstotbnd3  33705  heiborlem6  33745  rngosn3  33853  atlatmstc  34924  atlatle  34925  glbconN  34981  intnatN  35011  lnnat  35031  atcvrj2b  35036  atexchcvrN  35044  llncvrlpln  35162  lplncvrlvol  35220  lautcvr  35696  trlatn0  35777  cdleme48fvg  36105  cdlemg33c  36313  dihcl  36876  elpell1qr2  37753  oddcomabszz  37826  wepwsolem  37929  mendring  38079  mendlmod  38080  hausgraph  38107  rp-isfinite5  38180  cncmpmax  39505  eliinid  39608  icccncfext  40418  dvnprodlem2  40480  stoweidlem7  40542  stoweidlem34  40569  stoweidlem35  40570  stoweidlem59  40594  stoweidlem60  40595  stoweidlem62  40597  fourierdlem34  40676  fourierdlem73  40714  fourierdlem77  40718  etransclem35  40804  smfsuplem2  41339  pgrple2abl  42471
  Copyright terms: Public domain W3C validator