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

Theorem syl3an3b 1223
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 188 . 2  |-  ( ph  ->  th )
3 syl3an3b.2 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ta )
42, 3syl3an3 1220 1  |-  ( ( ps  /\  ch  /\  ph )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ w3a 937
This theorem is referenced by:  fresaunres1  5645  fvun2  5824  nnmsucr  6897  xrlttr  10764  iccdil  11065  icccntr  11067  absexpz  12141  posglbd  14607  isdrngd  15891  unicld  17141  2ndcdisj2  17551  logrec  20692  cdj3lem3  23972  f1omvdco3  27407  stoweidlem14  27777  bnj563  29209  bnj1033  29436
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator