Theorem syl3anb 1163

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

Syntax hints:   → wi 4   ↔ wb 196   ∧ w3a 1070

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 383  df-3an 1072

This theorem is referenced by:  syl3anbr  1164  poxp  7439  infempty  8567  symgsssg  18093  symgfisg  18094  lmodvscl  19089  xrs1mnd  19998  iscnp2  21263  clwwlknccat  27218  slmdvscl  30101  cgr3permute3  32485  cgr3permute1  32486  cgr3permute2  32487  cgr3permute4  32488  cgr3permute5  32489  colinearxfr  32513  grposnOLD  34006  rngunsnply  38262