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

Theorem syl3anb 1227
 Description: A triple syllogism inference. (Contributed by NM, 15-Oct-2005.)
Hypotheses
Ref Expression
syl3anb.1
syl3anb.2
syl3anb.3
syl3anb.4
Assertion
Ref Expression
syl3anb

Proof of Theorem syl3anb
StepHypRef Expression
1 syl3anb.1 . . 3
2 syl3anb.2 . . 3
3 syl3anb.3 . . 3
41, 2, 33anbi123i 1142 . 2
5 syl3anb.4 . 2
64, 5sylbi 188 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177   w3a 936 This theorem is referenced by:  syl3anbr  1228  poxp  6458  lmodvscl  15967  xrs1mnd  16736  iscnp2  17303  nb3grapr  21462  grposn  21803  cgr3permute3  25981  cgr3permute1  25982  cgr3permute2  25983  cgr3permute4  25984  cgr3permute5  25985  colinearxfr  26009  rngunsnply  27355  symgsssg  27385  symgfisg  27386 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8 This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938
 Copyright terms: Public domain W3C validator