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
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 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