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

Theorem syl3anb 1158
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 1152 . 2 ((𝜑𝜒𝜏) ↔ (𝜓𝜃𝜂))
5 syl3anb.4 . 2 ((𝜓𝜃𝜂) → 𝜁)
64, 5sylbi 216 1 ((𝜑𝜒𝜏) → 𝜁)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  w3a 1084
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 206  df-an 396  df-3an 1086
This theorem is referenced by:  syl3anbr  1159  poxp  8108  infempty  9497  symgsssg  19372  symgfisg  19373  lmodvscl  20709  xrs1mnd  21262  iscnp2  23053  clwwlknccat  29740  slmdvscl  32786  cgr3permute3  35480  cgr3permute1  35481  cgr3permute2  35482  cgr3permute4  35483  cgr3permute5  35484  colinearxfr  35508  grposnOLD  37206  rngunsnply  42370
  Copyright terms: Public domain W3C validator