Theorem syl3anb 1179

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  syl3anbr  1180  poxp  8126  infempty  9472  symgsssg  19561  symgfisg  19562  lmodvscl  21029  xrs1mnd  21620  iscnp2  23426  elreno2  28719  clwwlknccat  30457  slmdvscl  33574  cgr3permute3  36552  cgr3permute1  36553  cgr3permute2  36554  cgr3permute4  36555  cgr3permute5  36556  colinearxfr  36580  grposnOLD  38566  rngunsnply  43929