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

Theorem syl5com 26
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 22 . 2  |-  ( ph  ->  ( ch  ->  ps ) )
3 syl5com.2 . 2  |-  ( ch 
->  ( ps  ->  th )
)
42, 3sylcom 25 1  |-  ( ph  ->  ( ch  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  com12  27  syl5  28  ax16i  1999  ceqsalg  2825  cgsexg  2832  cgsex2g  2833  cgsex4g  2834  spc2egv  2883  spc3egv  2885  disjne  3513  uneqdifeq  3555  triun  4142  ordelord  4430  sucssel  4501  ordsuc  4621  tfi  4660  relresfld  5215  relcoi1  5217  unixpid  5223  fvimacnv  5656  fornex  5766  f1dmex  5767  tz7.49  6473  oeworde  6607  undifixp  6868  dom2d  6918  2pwuninel  7032  findcard  7113  fisupg  7121  dffi3  7200  noinfep  7376  cantnflem2  7408  tcmin  7442  rankr1ag  7490  rankpwi  7511  rankelb  7512  rankunb  7538  rankxpsuc  7568  alephordi  7717  alephsucdom  7722  alephinit  7738  dfac9  7778  ackbij2lem4  7884  cff1  7900  cfslbn  7909  cfcoflem  7914  cfcof  7916  infpssrlem5  7949  isfin7-2  8038  acncc  8082  domtriomlem  8084  axdc3lem2  8093  ttukeylem1  8152  iundom2g  8178  wunex2  8376  grupr  8435  gruiun  8437  eltskm  8481  nqereu  8569  addcanpr  8686  axpre-sup  8807  nneo  10111  zeo2  10114  xrub  10646  uznfz  10881  facndiv  11317  fsumcom2  12253  incexclem  12311  isumrpcl  12318  ndvdssub  12622  eucalglt  12771  prmind2  12785  coprm  12795  prmdiveq  12870  drsdir  14085  lubid  14132  istos  14157  latlem  14170  tsrlin  14344  dirge  14375  mhmlin  14438  issubg2  14652  nsgbi  14664  sylow2a  14946  issubrg2  15581  abvmul  15610  abvtri  15611  lmodlema  15648  lspsnel6  15767  lmhmlin  15808  lbsind  15849  cygth  16541  ipcj  16554  obsip  16637  inopn  16661  basis1  16704  tgss  16722  tgcl  16723  elcls3  16836  neindisj2  16876  cnpco  17012  cncls  17019  1stcelcls  17203  txkgen  17362  qtoptop2  17406  nrmr0reg  17456  fbasssin  17547  fbfinnfr  17552  fbunfip  17580  filufint  17631  uffix  17632  ufinffr  17640  ufilen  17641  fmfnfmlem1  17665  flftg  17707  alexsubALT  17761  xmeteq0  17919  blssex  17989  mopni3  18056  neibl  18063  metss  18070  metcnp3  18102  nmvs  18203  reperflem  18339  iccntr  18342  reconnlem2  18348  lebnumlem3  18477  caubl  18749  bcthlem5  18766  ovolunlem1  18872  voliunlem1  18923  volsuplem  18928  ellimc3  19245  lhop1lem  19376  ulmss  19790  dchrisumlema  20653  ablocom  20968  rngodm1dm2  21101  rngoueqz  21113  ubthlem1  21465  shaddcl  21812  shmulcl  21813  shmulclOLD  21814  spansnss2  22170  cnopc  22509  cnfnc  22526  adj1  22529  pjorthcoi  22765  stj  22831  mdsl1i  22917  chirredlem1  22986  mdsymlem5  23003  cdj3lem2b  23033  pconcn  23770  cvmlift2lem1  23848  relin01  24104  dfon2lem6  24215  wfrlem4  24330  wfrlem10  24336  frrlem4  24355  nofv  24382  nodenselem4  24409  waj-ax  24925  lukshef-ax2  24926  ontgval  24942  copsexgb  25069  domfldref  25164  f1ofi  25173  inttrp  25211  prjpacp1  25230  prjpacp2  25231  repcpwti  25264  labss1  25292  labss2  25294  domrancur1c  25305  prodeq3ii  25411  grpodivone  25476  rngmgmbs3  25520  rngodmeqrn  25522  zerdivemp1  25539  rngoridfz  25540  vecax5c  25586  svli2  25587  svs2  25590  truni3  25610  unint2t  25621  osneisi  25634  intopcoaconlem3b  25641  exopcopn  25675  limptlimpr2lem1  25677  limptlimpr2lem2  25678  intvconlem1  25806  hdrmp  25809  imonclem  25916  inttaror  26003  prismorcsetlemc  26020  codcatfun  26037  grphidmor2  26056  cmpmor  26078  lemindclsbu  26098  pgapspf  26155  nn0prpw  26342  heiborlem1  26638  zerdivemp1x  26689  isdrngo3  26693  0rngo  26755  pridl  26765  ispridlc  26798  isdmn3  26802  dmnnzd  26803  dfac21  27267  lindsss  27397  hashgt12el2  28219  uvtxisvtx  28303  usgrnloop  28351  eupatrl  28385  usgrcyclnl2  28387  eexinst11  28589  a9e2eq  28622  e222  28713  e111  28751  eel2221  28781  eel1111  28809  eel11111  28812  e333  28822  ax16iNEW7  29526  a12study10n  29759  lshpcmp  29800  omllaw  30055  dochexmidlem7  32278  lspindp5  32582
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator