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  1986  ceqsalg  2812  cgsexg  2819  cgsex2g  2820  cgsex4g  2821  spc2egv  2870  spc3egv  2872  disjne  3500  uneqdifeq  3542  triun  4126  ordelord  4414  sucssel  4485  ordsuc  4605  tfi  4644  relresfld  5199  relcoi1  5201  unixpid  5207  fvimacnv  5640  fornex  5750  f1dmex  5751  tz7.49  6457  oeworde  6591  undifixp  6852  dom2d  6902  2pwuninel  7016  findcard  7097  fisupg  7105  dffi3  7184  noinfep  7360  cantnflem2  7392  tcmin  7426  rankr1ag  7474  rankpwi  7495  rankelb  7496  rankunb  7522  rankxpsuc  7552  alephordi  7701  alephsucdom  7706  alephinit  7722  dfac9  7762  ackbij2lem4  7868  cff1  7884  cfslbn  7893  cfcoflem  7898  cfcof  7900  infpssrlem5  7933  isfin7-2  8022  acncc  8066  domtriomlem  8068  axdc3lem2  8077  ttukeylem1  8136  iundom2g  8162  wunex2  8360  grupr  8419  gruiun  8421  eltskm  8465  nqereu  8553  addcanpr  8670  axpre-sup  8791  nneo  10095  zeo2  10098  xrub  10630  uznfz  10865  facndiv  11301  fsumcom2  12237  incexclem  12295  isumrpcl  12302  ndvdssub  12606  eucalglt  12755  prmind2  12769  coprm  12779  prmdiveq  12854  drsdir  14069  lubid  14116  istos  14141  latlem  14154  tsrlin  14328  dirge  14359  mhmlin  14422  issubg2  14636  nsgbi  14648  sylow2a  14930  issubrg2  15565  abvmul  15594  abvtri  15595  lmodlema  15632  lspsnel6  15751  lmhmlin  15792  lbsind  15833  cygth  16525  ipcj  16538  obsip  16621  inopn  16645  basis1  16688  tgss  16706  tgcl  16707  elcls3  16820  neindisj2  16860  cnpco  16996  cncls  17003  1stcelcls  17187  txkgen  17346  qtoptop2  17390  nrmr0reg  17440  fbasssin  17531  fbfinnfr  17536  fbunfip  17564  filufint  17615  uffix  17616  ufinffr  17624  ufilen  17625  fmfnfmlem1  17649  flftg  17691  alexsubALT  17745  xmeteq0  17903  blssex  17973  mopni3  18040  neibl  18047  metss  18054  metcnp3  18086  nmvs  18187  reperflem  18323  iccntr  18326  reconnlem2  18332  lebnumlem3  18461  caubl  18733  bcthlem5  18750  ovolunlem1  18856  voliunlem1  18907  volsuplem  18912  ellimc3  19229  lhop1lem  19360  ulmss  19774  dchrisumlema  20637  ablocom  20952  rngodm1dm2  21085  rngoueqz  21097  ubthlem1  21449  shaddcl  21796  shmulcl  21797  shmulclOLD  21798  spansnss2  22154  cnopc  22493  cnfnc  22510  adj1  22513  pjorthcoi  22749  stj  22815  mdsl1i  22901  chirredlem1  22970  mdsymlem5  22987  cdj3lem2b  23017  pconcn  23755  cvmlift2lem1  23833  relin01  24089  dfon2lem6  24144  wfrlem4  24259  wfrlem10  24265  frrlem4  24284  nofv  24311  nodenselem4  24338  waj-ax  24853  lukshef-ax2  24854  ontgval  24870  copsexgb  24966  domfldref  25061  f1ofi  25070  inttrp  25108  prjpacp1  25127  prjpacp2  25128  repcpwti  25161  labss1  25189  labss2  25191  domrancur1c  25202  prodeq3ii  25308  grpodivone  25373  rngmgmbs3  25417  rngodmeqrn  25419  zerdivemp1  25436  rngoridfz  25437  vecax5c  25483  svli2  25484  svs2  25487  truni3  25507  unint2t  25518  osneisi  25531  intopcoaconlem3b  25538  exopcopn  25572  limptlimpr2lem1  25574  limptlimpr2lem2  25575  intvconlem1  25703  hdrmp  25706  imonclem  25813  inttaror  25900  prismorcsetlemc  25917  codcatfun  25934  grphidmor2  25953  cmpmor  25975  lemindclsbu  25995  pgapspf  26052  nn0prpw  26239  heiborlem1  26535  zerdivemp1x  26586  isdrngo3  26590  0rngo  26652  pridl  26662  ispridlc  26695  isdmn3  26699  dmnnzd  26700  dfac21  27164  lindsss  27294  uvtxisvtx  28162  eexinst11  28290  a9e2eq  28323  e222  28408  e111  28446  eel2221  28476  e333  28508  a12study10n  29137  lshpcmp  29178  omllaw  29433  dochexmidlem7  31656  lspindp5  31960
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator