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

Theorem syl3anb 1225
 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 1140 . 2
5 syl3anb.4 . 2
64, 5sylbi 187 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 176   w3a 934 This theorem is referenced by:  syl3anbr  1226  poxp  6243  lmodvscl  15660  xrs1mnd  16425  iscnp2  16985  grposn  20898  cgr3permute3  24742  cgr3permute1  24743  cgr3permute2  24744  cgr3permute4  24745  cgr3permute5  24746  colinearxfr  24770  conttnf2  25665  cmptdst  25671  rngunsnply  27481  symgsssg  27511  symgfisg  27512  nb3grapr  28289 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 177  df-an 360  df-3an 936
 Copyright terms: Public domain W3C validator