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  1595  ax9  1889  ax16i  1986  ax16ALT2  1988  wefrc  4387  ordzsl  4636  limuni3  4643  elres  4990  funcnvuni  5317  funrnex  5747  soxp  6228  sorpssuni  6286  sorpssint  6287  oaabs  6642  eceqoveq  6763  php3  7047  pssinf  7073  unbnn2  7114  inf0  7322  inf3lem5  7333  tcel  7430  rankxpsuc  7552  carduni  7614  prdom2  7636  dfac5  7755  cflm  7876  indpi  8531  prlem934  8657  xrub  10630  basis2  16689  fbdmn0  17529  rngoueqz  21097  atcv0eq  22959  dfon2lem9  24147  trpredrec  24241  frmin  24242  wfrlem4  24259  wfrlem10  24265  wfrlem12  24267  frrlem4  24284  frrlem11  24293  altopthsn  24495  rankeq1o  24801  imgfldref2  25064  eqfnung2  25118  prjmapcp2  25170  ridlideq  25335  svli2  25484  bwt2  25592  hdrmp  25706  fnctartar  25907  fnctartar2  25908  hbtlem5  27332  funressnfv  27991  afvco2  28037  ndmaovcl  28063  usgranloop  28124  nbgranself2  28151  ax9vax9  29158
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator