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

Theorem syl6com 34
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 32 . 2  |-  ( ph  ->  ( ps  ->  th )
)
43com12 30 1  |-  ( ps 
->  ( ph  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  19.33b  1619  a9e  1955  ax9OLD  2036  ax16i  2054  equveli  2088  ax16ALT2  2161  wefrc  4605  ordzsl  4854  limuni3  4861  elres  5210  funcnvuni  5547  funrnex  5996  soxp  6488  sorpssuni  6560  sorpssint  6561  oaabs  6916  eceqoveq  7038  php3  7322  pssinf  7348  unbnn2  7393  inf0  7605  inf3lem5  7616  tcel  7713  rankxpsuc  7837  carduni  7899  prdom2  7921  dfac5  8040  cflm  8161  indpi  8815  prlem934  8941  xrub  10921  injresinjlem  11230  hashgt12el  11713  hashgt12el2  11714  brfi1uzind  11746  basis2  17047  bwth  17504  fbdmn0  17897  usgranloopv  21429  nbgranself2  21479  usgrnloop  21594  wlkdvspthlem  21638  rngoueqz  22049  atcv0eq  23913  dfon2lem9  25449  trpredrec  25547  frmin  25548  wfrlem4  25572  wfrlem12  25580  frrlem4  25616  frrlem11  25625  altopthsn  25837  rankeq1o  26143  hbtlem5  27347  funressnfv  28006  afvco2  28054  ndmaovcl  28081  cshwssize  28348  4cyclusnfrgra  28507  frgrancvvdeqlem7  28523  frgrawopreglem2  28532  ax9NEW7  29566  ax16iNEW7  29649  ax16ALT2OLD7  29841
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
  Copyright terms: Public domain W3C validator