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  1701  ax6e  2007  axc16i  2068  rgen2a  2881  wefrc  4862  elres  5297  sorpssuni  6562  sorpssint  6563  ordzsl  6653  limuni3  6660  funcnvuni  6726  funrnex  6740  soxp  6886  oaabs  7285  eceqoveq  7408  php3  7696  pssinf  7723  unbnn2  7769  inf0  8029  inf3lem5  8040  tcel  8167  rankxpsuc  8291  carduni  8353  prdom2  8375  dfac5  8500  cflm  8621  indpi  9274  prlem934  9400  xrub  11506  injresinjlem  11906  hashgt12el  12465  hashgt12el2  12466  brfi1uzind  12516  cshwcsh2id  12787  cshwshash  14673  symgextf1  16645  gsummoncoe1  18541  basis2  19619  fbdmn0  20501  usgranloopv  24580  nbgranself2  24638  usgrnloop  24767  wlkdvspthlem  24811  4cyclusnfrgra  25221  frgrancvvdeqlem7  25238  rngoueqz  25630  atcv0eq  27496  dfon2lem9  29463  trpredrec  29561  frmin  29562  wfrlem4  29586  wfrlem12  29594  frrlem4  29630  frrlem11  29639  altopthsn  29839  rankeq1o  30056  wl-orel12  30209  wl-equsb4  30245  hbtlem5  31318  funressnfv  32452  afvco2  32500  ndmaovcl  32527  rngdir  32942  zlmodzxznm  33352
  Copyright terms: Public domain W3C validator