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

Theorem syl3anb 1366
 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 1249 . 2 ((𝜑𝜒𝜏) ↔ (𝜓𝜃𝜂))
5 syl3anb.4 . 2 ((𝜓𝜃𝜂) → 𝜁)
64, 5sylbi 207 1 ((𝜑𝜒𝜏) → 𝜁)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ w3a 1036 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 197  df-an 386  df-3an 1038 This theorem is referenced by:  syl3anbr  1367  poxp  7249  infempty  8372  symgsssg  17827  symgfisg  17828  lmodvscl  18820  xrs1mnd  19724  iscnp2  20983  slmdvscl  29594  cgr3permute3  31849  cgr3permute1  31850  cgr3permute2  31851  cgr3permute4  31852  cgr3permute5  31853  colinearxfr  31877  grposnOLD  33352  rngunsnply  37263
 Copyright terms: Public domain W3C validator