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

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

Proof of Theorem sylanr2
StepHypRef Expression
1 sylanr2.1 . . 3  |-  ( ph  ->  th )
21anim2i 554 . 2  |-  ( ( ch  /\  ph )  ->  ( ch  /\  th ) )
3 sylanr2.2 . 2  |-  ( ( ps  /\  ( ch 
/\  th ) )  ->  ta )
42, 3sylan2 462 1  |-  ( ( ps  /\  ( ch 
/\  ph ) )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360
This theorem is referenced by:  adantrrl  706  adantrrr  707  1stconst  6437  2ndconst  6438  isfin7-2  8278  mulsub  9478  fzsubel  11090  expsub  11429  ramlb  13389  0ram  13390  ressmplvsca  16524  tgcl  17036  fgss2  17908  nmoid  18778  chirredlem4  23898  pridlc3  26685  stoweidlem34  27761
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 179  df-an 362
  Copyright terms: Public domain W3C validator