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

Theorem sylancom 698
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 691 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 196  df-an 385
This theorem is referenced by:  adant423OLD  819  sofld  5500  ordin  5670  fimacnvdisj  5996  f1oexrnex  7008  wemoiso  7044  wemoiso2  7045  smorndom  7352  rdglim  7409  oaabs  7611  ssct  7926  onomeneq  8035  domfi  8066  f1vrnfibi  8134  brwdom2  8361  infdiffi  8438  cantnflem1  8469  wemapwe  8477  cnfcom3lem  8483  r1lim  8518  carduni  8690  ac5num  8742  infunsdom1  8918  cofsmo  8974  isf32lem6  9063  hsmexlem1  9131  ac6c4  9186  pwfseqlem1  9359  tskuni  9484  recgt1i  10799  avgle2  11150  eluzmn  11570  rpnnen1lem1  11691  rpnnen1lem1OLD  11697  ioodisj  12173  fzneuz  12290  mulmod0  12538  hasheni  12998  hashun2  13033  swrdccatin1  13334  reccn2  14175  isershft  14242  sumeq2ii  14271  prodeq2ii  14482  demoivreALT  14770  bitsp1  14991  gcdneg  15081  eucalginv  15135  eucalg  15138  odzdvds  15338  fldivp1  15439  prmunb  15456  vdwap1  15519  setsid  15742  funcsetcestrclem7  16624  acsmapd  17001  intopsn  17076  cntzidss  17593  symggrp  17643  odmodnn0  17782  sylow2alem1  17855  telgsumfzs  18209  dprdsn  18258  dvdsrmul1  18476  dvrid  18511  evl1val  19514  evl1sca  19519  pf1const  19531  znunit  19731  isphld  19818  frlmup1  19956  mat1f1o  20103  mat1mhm  20109  matunit  20303  pm2mpmhmlem2  20443  cctop  20620  iscnp4  20877  iscncl  20883  cnntr  20889  tx2cn  21223  xkoco1cn  21270  qtopkgen  21323  hmeontr  21382  hmeores  21384  filssufilg  21525  ustuqtop1  21855  ustuqtop2  21856  utop2nei  21864  fmucndlem  21905  cfilufg  21907  xmetres2  21976  metres2  21978  metustto  22168  cfilucfil  22174  dscopn  22188  nmoi  22342  iccntr  22432  cphsqrtcl2  22794  cmsss  22955  ivthlem3  23029  sca2rab  23087  ovolicc2lem3  23094  mdegleb  23628  aalioulem3  23893  ulm2  23943  ulmcn  23957  root1eq1  24296  atanlogsublem  24442  birthdaylem3  24480  logexprlim  24750  dchrisumlem3  24980  tglowdim1i  25196  f1otrg  25551  f1otrge  25552  ax5seglem1  25608  ax5seglem2  25609  ax5seglem3a  25610  ax5seglem4  25612  ax5seglem9  25617  ax5seg  25618  axbtwnid  25619  axlowdimlem17  25638  axcontlem2  25645  axcontlem4  25647  axcontlem8  25651  constr3trllem2  26179  vdgrnn0pnf  26436  rusgranumwlks  26483  eupatrl  26495  grpoidinv  26746  imsmetlem  26929  ipasslem1  27070  ip2eqi  27096  hvpncan  27280  pjid  27938  hmopre  28166  eigvalcl  28204  leopnmid  28381  superpos  28597  cvp  28618  rabfodom  28728  fnct  28876  xlt2addrd  28913  lmodslmd  29088  locfinreflem  29235  prsdm  29288  prsrn  29289  fmcncfil  29305  rge0scvg  29323  esumfsup  29459  esumcvg  29475  insiga  29527  ballotlemirc  29920  signstfvcl  29976  subfacp1lem6  30421  msubff1  30707  fv2ndcnv  30926  matunitlindf  32577  ovoliunnfl  32621  voliunnfl  32623  volsupnfl  32624  ftc1anclem5  32659  indexa  32698  sstotbnd3  32745  heiborlem6  32785  rngosn3  32893  atlatmstc  33624  atlatle  33625  glbconN  33681  intnatN  33711  lnnat  33731  atcvrj2b  33736  atexchcvrN  33744  llncvrlpln  33862  lplncvrlvol  33920  lautcvr  34396  trlatn0  34477  cdleme48fvg  34806  cdlemg33c  35014  dihcl  35577  elpell1qr2  36454  oddcomabszz  36527  wepwsolem  36630  mendring  36781  mendlmod  36782  hausgraph  36809  rp-isfinite5  36882  cncmpmax  38214  icccncfext  38773  dvnprodlem2  38837  stoweidlem7  38900  stoweidlem34  38927  stoweidlem35  38928  stoweidlem59  38952  stoweidlem60  38953  stoweidlem62  38955  fourierdlem34  39034  fourierdlem73  39072  fourierdlem77  39076  etransclem35  39162  rusgrnumwwlks  41177  pgrple2abl  41940
  Copyright terms: Public domain W3C validator