Theorem syl3anb 1162

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 1156	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) ↔ (𝜓 ∧ 𝜃 ∧ 𝜂))
5		syl3anb.4	. 2 ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) → 𝜁)
6	4, 5	sylbi 217	1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜁)

Syntax hints:   → wi 4   ↔ wb 206   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  syl3anbr  1163  poxp  8071  infempty  9415  symgsssg  19433  symgfisg  19434  lmodvscl  20864  xrs1mnd  21430  iscnp2  23214  elreno2  28501  clwwlknccat  30148  slmdvscl  33290  cgr3permute3  36245  cgr3permute1  36246  cgr3permute2  36247  cgr3permute4  36248  cgr3permute5  36249  colinearxfr  36273  grposnOLD  38217  rngunsnply  43615