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

Theorem syl9 71
Description: A nested syllogism inference with different antecedents. (Contributed by NM, 13-May-1993.) (Proof shortened by Josh Purinton, 29-Dec-2000.)
Hypotheses
Ref Expression
syl9.1  |-  ( ph  ->  ( ps  ->  ch ) )
syl9.2  |-  ( th 
->  ( ch  ->  ta ) )
Assertion
Ref Expression
syl9  |-  ( ph  ->  ( th  ->  ( ps  ->  ta ) ) )

Proof of Theorem syl9
StepHypRef Expression
1 syl9.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
2 syl9.2 . . 3  |-  ( th 
->  ( ch  ->  ta ) )
32a1i 11 . 2  |-  ( ph  ->  ( th  ->  ( ch  ->  ta ) ) )
41, 3syl5d 67 1  |-  ( ph  ->  ( th  ->  ( ps  ->  ta ) ) )
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:  syl9r  72  com23  78  sylan9  655  19.21t  1912  axc9lem1  2008  axc9lem2  2046  axc11n  2055  axc11nOLD  2056  sbequi  2120  reuss2  3703  reupick  3707  ordtr2  4836  suc11  4895  elres  5221  funimass4  5825  fliftfun  6111  omlimcl  7145  nneob  7219  rankwflemb  8124  cflm  8543  domtriomlem  8735  grothomex  9118  sup3  10416  caubnd  13193  fbflim2  20563  ellimc3  22368  3cyclfrgrarn1  25133  dfon2lem6  29385  opnrebl2  30305  pm11.71  31471  axc11next  31481  bj-axc11nv  34663  stdpc5t  34747  diaintclN  37198  dibintclN  37307  dihintcl  37484
  Copyright terms: Public domain W3C validator