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

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

Proof of Theorem syl6com
StepHypRef Expression
1 syl6com.1 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
2 syl6com.2 . . 3  |-  ( ch 
->  th )
31, 2syl6 33 . 2  |-  ( ph  ->  ( ps  ->  th )
)
43com12 31 1  |-  ( ps 
->  ( ph  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  19.33b  1673  ax6e  1971  axc16i  2037  rgen2a  2891  wefrc  4873  elres  5309  sorpssuni  6574  sorpssint  6575  ordzsl  6665  limuni3  6672  funcnvuni  6738  funrnex  6752  soxp  6897  oaabs  7294  eceqoveq  7417  php3  7704  pssinf  7731  unbnn2  7778  inf0  8039  inf3lem5  8050  tcel  8177  rankxpsuc  8301  carduni  8363  prdom2  8385  dfac5  8510  cflm  8631  indpi  9286  prlem934  9412  xrub  11504  injresinjlem  11894  hashgt12el  12447  hashgt12el2  12448  brfi1uzind  12499  cshwcsh2id  12762  cshwshash  14450  symgextf1  16260  gsummoncoe1  18157  basis2  19259  bwthOLD  19717  fbdmn0  20162  usgranloopv  24151  nbgranself2  24209  usgrnloop  24338  wlkdvspthlem  24382  4cyclusnfrgra  24792  frgrancvvdeqlem7  24810  frgrawopreglem2  24819  rngoueqz  25205  atcv0eq  27071  dfon2lem9  29076  trpredrec  29174  frmin  29175  wfrlem4  29199  wfrlem12  29207  frrlem4  29243  frrlem11  29252  altopthsn  29464  rankeq1o  29681  wl-equsb4  29858  hbtlem5  30908  funressnfv  31907  afvco2  31955  ndmaovcl  31982  zlmodzxznm  32396
  Copyright terms: Public domain W3C validator