MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl5com Unicode version

Theorem syl5com 30
Description: Syllogism inference with commuted antecedents. (Contributed by NM, 24-May-2005.)
Hypotheses
Ref Expression
syl5com.1
syl5com.2
Assertion
Ref Expression
syl5com

Proof of Theorem syl5com
StepHypRef Expression
1 syl5com.1 . . 3
21a1d 25 . 2
3 syl5com.2 . 2
42, 3sylcom 29 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4
This theorem is referenced by:  com12  31  syl5  32  speimfw  1735  axc11nlem  1938  axc11nlemOLD  2048  axc11n  2049  axc11nOLD  2050  axc16i  2064  mo2vOLD  2290  mo2vOLDOLD  2291  eupickbi  2361  2moOLD  2374  ceqsalgALT  3135  cgsexg  3142  cgsex2g  3143  cgsex4g  3144  spc2egv  3196  spc3egv  3198  disjne  3872  uneqdifeq  3916  triun  4558  sucssel  4975  relresfld  5539  relcoi1  5541  unixpid  5547  fvimacnv  6002  ordsuc  6649  tfi  6688  fornex  6769  f1ovv  6771  tz7.49  7129  oeworde  7261  undifixp  7525  dom2d  7576  findcard  7779  fisupg  7788  dffi3  7911  noinfep  8097  cantnflem2  8130  tcmin  8193  rankr1ag  8241  rankpwi  8262  rankelb  8263  rankunb  8289  rankxpsuc  8321  alephordi  8476  alephsucdom  8481  alephinit  8497  dfac9  8537  ackbij2lem4  8643  cff1  8659  cfslbn  8668  cfcoflem  8673  cfcof  8675  infpssrlem5  8708  isfin7-2  8797  acncc  8841  domtriomlem  8843  axdc3lem2  8852  ttukeylem1  8910  iundom2g  8936  axpowndlem3  8996  wunex2  9137  grupr  9196  gruiun  9198  eltskm  9242  nqereu  9328  addcanpr  9445  axpre-sup  9567  relin01  10102  nneo  10971  zeo2  10974  xrub  11532  uznfz  11790  difelfzle  11817  ssfzo12  11905  facndiv  12366  hashf1rn  12425  hashgt12el2  12482  hash2prde  12516  hash2prd  12518  hash2pwpr  12519  exprelprel  12528  brfi1uzind  12532  swrdswrd  12685  swrdccatin2  12712  swrdccatin12lem2  12714  swrdccatin12  12716  swrdccat3  12717  swrdccatid  12722  repswswrd  12756  2cshwcshw  12793  fsumcom2  13589  incexclem  13648  fprodss  13755  fprodcom2  13788  ndvdssub  14065  eucalglt  14214  prmind2  14228  coprm  14241  prmdiveq  14316  drsdir  15564  lublecllem  15618  istos  15665  tsrlin  15849  dirge  15867  mhmlin  15973  issubg2  16216  nsgbi  16232  symgextf1lem  16445  sylow2a  16639  issubrg2  17449  abvmul  17478  abvtri  17479  lmodlema  17517  lspsnel6  17640  lmhmlin  17681  lbsind  17726  0ring01eq  17919  01eq0ring  17920  gsummoncoe1  18346  cygth  18610  ipcj  18669  obsip  18752  lindsss  18859  mamufacex  18891  mavmulsolcl  19053  slesolvec  19181  inopn  19408  basis1  19451  tgss  19470  tgcl  19471  elcls3  19584  neindisj2  19624  cnpco  19768  cncls  19775  1stcelcls  19962  txkgen  20153  qtoptop2  20200  nrmr0reg  20250  fbasssin  20337  fbfinnfr  20342  fbunfip  20370  filufint  20421  uffix  20422  ufinffr  20430  ufilen  20431  fmfnfmlem1  20455  flftg  20497  alexsubALT  20551  xmeteq0  20841  blssexps  20929  blssex  20930  mopni3  20997  neibl  21004  metss  21011  metcnp3  21043  nmvs  21185  reperflem  21323  iccntr  21326  reconnlem2  21332  lebnumlem3  21463  caubl  21746  bcthlem5  21767  ovolunlem1  21908  voliunlem1  21960  volsuplem  21965  ellimc3  22283  lhop1lem  22414  ulmss  22792  dchrisumlema  23673  usgrarnedg  24384  usgrafisbase  24414  sizeusglecusglem1  24484  uvtxisvtx  24490  wlkn0  24527  usgrnloop  24565  usgra2wlkspthlem1  24619  usgrcyclnl2  24641  wlk0  24761  clwwlknprop  24772  clwlkisclwwlklem0  24788  wwlkext2clwwlk  24803  clwlkfclwwlk  24844  usgfiregdegfi  24911  eupatrl  24968  2pthfrgra  25011  3cyclfrgrarn2  25014  frgrancvvdeqlemB  25038  frgrawopreg1  25050  frgrawopreg2  25051  frgraeu  25054  numclwwlkovf2ex  25086  frgraregord013  25118  frgraogt3nreg  25120  ablocom  25287  rngodm1dm2  25420  rngoueqz  25432  zerdivemp1  25436  rngoridfz  25437  ubthlem1  25786  shaddcl  26134  shmulcl  26135  shmulclOLD  26136  spansnss2  26493  cnopc  26832  cnfnc  26849  adj1  26852  pjorthcoi  27088  stj  27154  mdsl1i  27240  chirredlem1  27309  mdsymlem5  27326  cdj3lem2b  27356  slmdlema  27746  pconcn  28669  cvmlift2lem1  28747  ss2mcls  28928  dfon2lem6  29220  wfrlem4  29346  wfrlem10  29352  frrlem4  29390  nofv  29417  nodenselem4  29444  waj-ax  29879  lukshef-ax2  29880  ontgval  29896  nn0prpw  30141  heiborlem1  30307  zerdivemp1x  30358  isdrngo3  30362  0rngo  30424  pridl  30434  ispridlc  30467  isdmn3  30471  dmnnzd  30472  dfac21  31012  2f1fvneq  32307  imarnf1pr  32309  2ffzoeq  32341  usgrauvtxvd  32358  usgo0s0  32435  usgo0s0ALT  32436  usgo1s0ALT  32437  usgo1s0  32442  usgresvm1  32443  usgresvm1ALT  32447  nrhmzr  32679  nzerooringczr  32880  gsumpr  32950  lincdifsn  33025  snlindsntor  33072  lincresunit3lem1  33080  lincresunit3lem2  33081  lincresunit3  33082  eexinst11  33297  ax6e2eq  33330  e222  33422  e111  33460  eel12131  33506  e333  33530  bj-alrim  34246  bj-nexdt  34250  bj-axc11nlemv  34315  bj-axc11nv  34316  lshpcmp  34713  omllaw  34968  dochexmidlem7  37193  lspindp5  37497
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
  Copyright terms: Public domain W3C validator