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

Theorem syl6com 36
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 34 . 2  |-  ( ph  ->  ( ps  ->  th )
)
43com12 32 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  1740  ax6e  2056  axc16i  2119  rgen2a  2852  wefrc  4844  elres  5156  sorpssuni  6591  sorpssint  6592  ordzsl  6683  limuni3  6690  funcnvuni  6757  funrnex  6771  soxp  6917  wfrlem4  7044  wfrlem12  7052  oaabs  7350  eceqoveq  7473  php3  7761  pssinf  7785  unbnn2  7831  inf0  8129  inf3lem5  8140  tcel  8231  rankxpsuc  8355  carduni  8417  prdom2  8439  dfac5  8560  cflm  8681  indpi  9333  prlem934  9459  negf1o  10050  xrub  11598  injresinjlem  12024  hashgt12el  12593  hashgt12el2  12594  brfi1uzind  12647  cshwcsh2id  12918  cshwshash  15063  symgextf1  17050  gsummoncoe1  18886  basis2  19953  fbdmn0  20836  usgranloopv  25092  nbgranself2  25150  usgrwlknloop  25279  wlkdvspthlem  25323  4cyclusnfrgra  25733  frgrancvvdeqlem7  25750  rngoueqz  26144  atcv0eq  28018  dfon2lem9  30432  trpredrec  30474  frmin  30475  frrlem4  30512  frrlem11  30521  altopthsn  30721  rankeq1o  30931  wl-orel12  31763  wl-equsb4  31799  hbtlem5  35907  funressnfv  38342  afvco2  38390  ndmaovcl  38417  bgoldbtbndlem4  38615  rngdir  39154  zlmodzxznm  39564
  Copyright terms: Public domain W3C validator