Theorem syl3anb 1161

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

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

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 1088

This theorem is referenced by:  syl3anbr  1162  poxp  8135  infempty  9529  symgsssg  19454  symgfisg  19455  lmodvscl  20845  xrs1mnd  21385  iscnp2  23194  clwwlknccat  30011  slmdvscl  33164  cgr3permute3  36023  cgr3permute1  36024  cgr3permute2  36025  cgr3permute4  36026  cgr3permute5  36027  colinearxfr  36051  grposnOLD  37864  rngunsnply  43159