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

Theorem syl3an3b 1222
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 187 . 2  |-  ( ph  ->  th )
3 syl3an3b.2 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ta )
42, 3syl3an3 1219 1  |-  ( ( ps  /\  ch  /\  ph )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ w3a 936
This theorem is referenced by:  fresaunres1  5579  fvun2  5758  nnmsucr  6831  xrlttr  10693  iccdil  10994  icccntr  10996  absexpz  12069  posglbd  14535  isdrngd  15819  unicld  17069  2ndcdisj2  17477  logrec  20618  cdj3lem3  23898  f1omvdco3  27264  stoweidlem14  27634  bnj563  28821  bnj1033  29048
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  df-3an 938
  Copyright terms: Public domain W3C validator