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

Theorem syl3an3b 1266
Description: A syllogism inference. (Contributed by NM, 22-Aug-1995.)
Hypotheses
Ref Expression
syl3an3b.1
syl3an3b.2
Assertion
Ref Expression
syl3an3b

Proof of Theorem syl3an3b
StepHypRef Expression
1 syl3an3b.1 . . 3
21biimpi 194 . 2
3 syl3an3b.2 . 2
42, 3syl3an3 1263 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\w3a 973
This theorem is referenced by:  fresaunres1  5763  fvun2  5945  nnmsucr  7293  xrlttr  11375  iccdil  11687  icccntr  11689  absexpz  13138  posglbd  15780  f1omvdco3  16474  isdrngd  17421  unicld  19547  2ndcdisj2  19958  logrec  23151  cdj3lem3  27357  stoweidlem14  31796  bnj563  33800  bnj1033  34025
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
  Copyright terms: Public domain W3C validator