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

Step	Hyp	Ref	Expression
1		syl3an3b.1	. . 3
2	1	biimpi 194	. 2
3		syl3an3b.2	. 2
4	2, 3	syl3an3 1263	1

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