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

Theorem syl5com 29
Description: Syllogism inference with commuted antecedents. (Contributed by NM, 24-May-2005.)
Hypotheses
Ref Expression
syl5com.1  |-  ( ph  ->  ps )
syl5com.2  |-  ( ch 
->  ( ps  ->  th )
)
Assertion
Ref Expression
syl5com  |-  ( ph  ->  ( ch  ->  th )
)

Proof of Theorem syl5com
StepHypRef Expression
1 syl5com.1 . . 3  |-  ( ph  ->  ps )
21a1d 24 . 2  |-  ( ph  ->  ( ch  ->  ps ) )
3 syl5com.2 . 2  |-  ( ch 
->  ( ps  ->  th )
)
42, 3sylcom 28 1  |-  ( ph  ->  ( ch  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  com12  30  syl5  31  ax10lem2  2024  ax10  2026  ax16i  2052  ceqsalg  2981  cgsexg  2988  cgsex2g  2989  cgsex4g  2990  spc2egv  3039  spc3egv  3041  disjne  3674  uneqdifeq  3717  triun  4316  ordelord  4604  sucssel  4675  ordsuc  4795  tfi  4834  relresfld  5397  relcoi1  5399  unixpid  5405  fvimacnv  5846  fornex  5971  f1dmex  5972  tz7.49  6703  oeworde  6837  undifixp  7099  dom2d  7149  2pwuninel  7263  findcard  7348  fisupg  7356  dffi3  7437  noinfep  7615  cantnflem2  7647  tcmin  7681  rankr1ag  7729  rankpwi  7750  rankelb  7751  rankunb  7777  rankxpsuc  7807  alephordi  7956  alephsucdom  7961  alephinit  7977  dfac9  8017  ackbij2lem4  8123  cff1  8139  cfslbn  8148  cfcoflem  8153  cfcof  8155  infpssrlem5  8188  isfin7-2  8277  acncc  8321  domtriomlem  8323  axdc3lem2  8332  ttukeylem1  8390  iundom2g  8416  wunex2  8614  grupr  8673  gruiun  8675  eltskm  8719  nqereu  8807  addcanpr  8924  axpre-sup  9045  nneo  10354  zeo2  10357  xrub  10891  uznfz  11131  facndiv  11580  hashf1rn  11637  hashgt12el2  11684  hash2prde  11689  brfi1uzind  11716  fsumcom2  12559  incexclem  12617  isumrpcl  12624  ndvdssub  12928  eucalglt  13077  prmind2  13091  coprm  13101  prmdiveq  13176  drsdir  14393  lubid  14440  istos  14465  latlem  14478  tsrlin  14652  dirge  14683  mhmlin  14746  issubg2  14960  nsgbi  14972  sylow2a  15254  issubrg2  15889  abvmul  15918  abvtri  15919  lmodlema  15956  lspsnel6  16071  lmhmlin  16112  lbsind  16153  cygth  16853  ipcj  16866  obsip  16949  inopn  16973  basis1  17016  tgss  17034  tgcl  17035  elcls3  17148  neindisj2  17188  cnpco  17332  cncls  17339  1stcelcls  17525  txkgen  17685  qtoptop2  17732  nrmr0reg  17782  fbasssin  17869  fbfinnfr  17874  fbunfip  17902  filufint  17953  uffix  17954  ufinffr  17962  ufilen  17963  fmfnfmlem1  17987  flftg  18029  alexsubALT  18083  xmeteq0  18369  blssexps  18457  blssex  18458  mopni3  18525  neibl  18532  metss  18539  metcnp3  18571  nmvs  18713  reperflem  18850  iccntr  18853  reconnlem2  18859  lebnumlem3  18989  caubl  19261  bcthlem5  19282  ovolunlem1  19394  voliunlem1  19445  volsuplem  19450  ellimc3  19767  lhop1lem  19898  ulmss  20314  dchrisumlema  21183  usgrarnedg  21405  usgrafisbase  21429  sizeusglecusglem1  21494  uvtxisvtx  21500  usgrnloop  21564  usgrcyclnl2  21629  eupatrl  21691  ablocom  21874  rngodm1dm2  22007  rngoueqz  22019  zerdivemp1  22023  rngoridfz  22024  ubthlem1  22373  shaddcl  22720  shmulcl  22721  shmulclOLD  22722  spansnss2  23078  cnopc  23417  cnfnc  23434  adj1  23437  pjorthcoi  23673  stj  23739  mdsl1i  23825  chirredlem1  23894  mdsymlem5  23911  cdj3lem2b  23941  pconcn  24912  cvmlift2lem1  24990  relin01  25195  fprodss  25275  fprodcom2  25309  dfon2lem6  25416  wfrlem4  25542  wfrlem10  25548  frrlem4  25586  nofv  25613  nodenselem4  25640  waj-ax  26165  lukshef-ax2  26166  ontgval  26182  nn0prpw  26327  heiborlem1  26521  zerdivemp1x  26572  isdrngo3  26576  0rngo  26638  pridl  26648  ispridlc  26681  isdmn3  26685  dmnnzd  26686  dfac21  27142  lindsss  27272  2f1fvneq  28078  imarnf1pr  28085  ssfzo12  28131  2ffzoeq  28141  swrdswrd  28200  swrdccatin2  28211  swrdccatin12lem3  28213  swrdccatin12  28215  swrdccat3  28216  2cshw1lem1  28249  2cshw2lem3  28255  cshweqrep  28275  cshwssizelem1a  28280  usgra2wlkspthlem1  28307  usgfiregdegfi  28362  usgrauvtxvd  28364  2pthfrgra  28402  3cyclfrgrarn2  28405  frgrancvvdeqlemB  28428  frgrawopreg1  28440  frgrawopreg2  28441  frgraeu  28444  eexinst11  28612  a9e2eq  28645  e222  28738  e111  28776  eel12131  28822  e333  28846  ax16iNEW7  29552  lshpcmp  29787  omllaw  30042  dochexmidlem7  32265  lspindp5  32569
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator