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

Theorem syl6com 33
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 31 . 2  |-  ( ph  ->  ( ps  ->  th )
)
43com12 29 1  |-  ( ps 
->  ( ph  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  19.33b  1615  a9e  1948  ax9OLD  1999  equveli  2042  ax16i  2095  ax16ALT2  2097  wefrc  4536  ordzsl  4784  limuni3  4791  elres  5140  funcnvuni  5477  funrnex  5926  soxp  6418  sorpssuni  6490  sorpssint  6491  oaabs  6846  eceqoveq  6968  php3  7252  pssinf  7278  unbnn2  7323  inf0  7532  inf3lem5  7543  tcel  7640  rankxpsuc  7762  carduni  7824  prdom2  7846  dfac5  7965  cflm  8086  indpi  8740  prlem934  8866  xrub  10846  injresinjlem  11154  hashgt12el  11637  hashgt12el2  11638  brfi1uzind  11670  basis2  16971  fbdmn0  17819  usgranloopv  21351  nbgranself2  21401  usgrnloop  21516  wlkdvspthlem  21560  rngoueqz  21971  atcv0eq  23835  dfon2lem9  25361  trpredrec  25455  frmin  25456  wfrlem4  25473  wfrlem10  25479  wfrlem12  25481  frrlem4  25498  frrlem11  25507  altopthsn  25710  rankeq1o  26016  hbtlem5  27200  funressnfv  27859  afvco2  27907  ndmaovcl  27934  4cyclusnfrgra  28123  frgrancvvdeqlem7  28139  frgrawopreglem2  28148  ax9NEW7  29174  ax16iNEW7  29255  ax16ALT2OLD7  29427
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator