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

Theorem syl3an3b 1257
Description: A syllogism inference. (Contributed by NM, 22-Aug-1995.)
Hypotheses
Ref Expression
syl3an3b.1  |-  ( ph  <->  th )
syl3an3b.2  |-  ( ( ps  /\  ch  /\  th )  ->  ta )
Assertion
Ref Expression
syl3an3b  |-  ( ( ps  /\  ch  /\  ph )  ->  ta )

Proof of Theorem syl3an3b
StepHypRef Expression
1 syl3an3b.1 . . 3  |-  ( ph  <->  th )
21biimpi 194 . 2  |-  ( ph  ->  th )
3 syl3an3b.2 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ta )
42, 3syl3an3 1254 1  |-  ( ( ps  /\  ch  /\  ph )  ->  ta )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ w3a 965
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 967
This theorem is referenced by:  fresaunres1  5695  fvun2  5875  nnmsucr  7177  xrlttr  11231  iccdil  11543  icccntr  11545  absexpz  12915  posglbd  15442  f1omvdco3  16077  isdrngd  16983  unicld  18785  2ndcdisj2  19196  logrec  22351  cdj3lem3  26014  stoweidlem14  29977  bnj563  32087  bnj1033  32312
  Copyright terms: Public domain W3C validator