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

Theorem syl6com 31
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 29 . 2  |-  ( ph  ->  ( ps  ->  th )
)
43com12 27 1  |-  ( ps 
->  ( ph  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  19.33b  1613  ax9  1962  ax16i  2059  ax16ALT2  2061  wefrc  4490  ordzsl  4739  limuni3  4746  elres  5093  funcnvuni  5422  funrnex  5867  soxp  6356  sorpssuni  6428  sorpssint  6429  oaabs  6784  eceqoveq  6906  php3  7190  pssinf  7216  unbnn2  7261  inf0  7469  inf3lem5  7480  tcel  7577  rankxpsuc  7699  carduni  7761  prdom2  7783  dfac5  7902  cflm  8023  indpi  8678  prlem934  8804  xrub  10783  injresinjlem  11086  hashgt12el  11569  hashgt12el2  11570  brfi1uzind  11602  basis2  16906  fbdmn0  17742  usgranloop  21076  nbgranself2  21118  rngoueqz  21529  atcv0eq  23393  dfon2lem9  24973  trpredrec  25067  frmin  25068  wfrlem4  25085  wfrlem10  25091  wfrlem12  25093  frrlem4  25110  frrlem11  25119  altopthsn  25322  rankeq1o  25628  hbtlem5  26923  funressnfv  27584  afvco2  27632  ndmaovcl  27659  usgrnloop  27718  wlkdvspthlem  27754  frgrancvvdeqlem7  27859  frgrawopreglem2  27868  ax9NEW7  28881  ax16iNEW7  28962  ax16ALT2OLD7  29134  ax9vax9  29217
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator