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

Theorem sylanl2 633
Description: A syllogism inference. (Contributed by NM, 1-Jan-2005.)
Hypotheses
Ref Expression
sylanl2.1  |-  ( ph  ->  ch )
sylanl2.2  |-  ( ( ( ps  /\  ch )  /\  th )  ->  ta )
Assertion
Ref Expression
sylanl2  |-  ( ( ( ps  /\  ph )  /\  th )  ->  ta )

Proof of Theorem sylanl2
StepHypRef Expression
1 sylanl2.1 . . 3  |-  ( ph  ->  ch )
21anim2i 553 . 2  |-  ( ( ps  /\  ph )  ->  ( ps  /\  ch ) )
3 sylanl2.2 . 2  |-  ( ( ( ps  /\  ch )  /\  th )  ->  ta )
42, 3sylan 458 1  |-  ( ( ( ps  /\  ph )  /\  th )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  mpanlr1  668  adantlrl  701  adantlrr  702  riotasv2dOLD  6554  oesuclem  6728  oelim  6737  mulsub  9432  divsubdiv  9686  vdwlem12  13315  dpjidcl  15571  cnextfun  18048  elbl4  18559  metucnOLD  18571  metucn  18572  dvradcnv  20290  dchrisum0lem2a  21164  cnlnadjlem2  23524  chirredlem2  23847  mdsymlem5  23863  sibfof  24607  axcontlem4  25810  unichnidl  26531  dmncan2  26577  jm2.26  26963  cvrexchlem  29901
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator