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

Step	Hyp	Ref	Expression
1		syl3anb.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2		syl3anb.2	. . 3 ⊢ (𝜒 ↔ 𝜃)
3		syl3anb.3	. . 3 ⊢ (𝜏 ↔ 𝜂)
4	1, 2, 3	3anbi123i 1152	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) ↔ (𝜓 ∧ 𝜃 ∧ 𝜂))
5		syl3anb.4	. 2 ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) → 𝜁)
6	4, 5	sylbi 216	1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜁)

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