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

Theorem syl3an3b 1220
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 186 . 2  |-  ( ph  ->  th )
3 syl3an3b.2 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ta )
42, 3syl3an3 1217 1  |-  ( ( ps  /\  ch  /\  ph )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ w3a 934
This theorem is referenced by:  fresaunres1  5497  fvun2  5674  nnmsucr  6710  xrlttr  10566  iccdil  10865  icccntr  10867  absexpz  11886  posglbd  14352  isdrngd  15636  unicld  16889  2ndcdisj2  17289  logrec  20228  cdj3lem3  23132  f1omvdco3  26715  stoweidlem14  27086  bnj563  28534  bnj1033  28761
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator