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

Theorem syl3an3b 1266
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 1263 1  |-  ( ( ps  /\  ch  /\  ph )  ->  ta )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ w3a 973
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 975
This theorem is referenced by:  fresaunres1  5764  fvun2  5946  nnmsucr  7286  xrlttr  11358  iccdil  11670  icccntr  11672  absexpz  13118  posglbd  15654  f1omvdco3  16347  isdrngd  17292  unicld  19415  2ndcdisj2  19826  logrec  23017  cdj3lem3  27171  stoweidlem14  31628  bnj563  33235  bnj1033  33460
  Copyright terms: Public domain W3C validator