Theorem an6 1474

Description: Rearrangement of 6 conjuncts. (Contributed by NM, 13-Mar-1995.)

Assertion

Ref	Expression
an6	⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂)) ↔ ((𝜑 ∧ 𝜃) ∧ (𝜓 ∧ 𝜏) ∧ (𝜒 ∧ 𝜂)))

Proof of Theorem an6

Step	Hyp	Ref	Expression
1		an4 669	. . 3 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ ((𝜃 ∧ 𝜏) ∧ 𝜂)) ↔ (((𝜑 ∧ 𝜓) ∧ (𝜃 ∧ 𝜏)) ∧ (𝜒 ∧ 𝜂)))
2		an4 669	. . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜃 ∧ 𝜏)) ↔ ((𝜑 ∧ 𝜃) ∧ (𝜓 ∧ 𝜏)))
3	1, 2	bianbi 639	. 2 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ ((𝜃 ∧ 𝜏) ∧ 𝜂)) ↔ (((𝜑 ∧ 𝜃) ∧ (𝜓 ∧ 𝜏)) ∧ (𝜒 ∧ 𝜂)))
4		df-3an 1105	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
5		df-3an 1105	. . 3 ⊢ ((𝜃 ∧ 𝜏 ∧ 𝜂) ↔ ((𝜃 ∧ 𝜏) ∧ 𝜂))
6	4, 5	anbi12i 640	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂)) ↔ (((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ ((𝜃 ∧ 𝜏) ∧ 𝜂)))
7		df-3an 1105	. 2 ⊢ (((𝜑 ∧ 𝜃) ∧ (𝜓 ∧ 𝜏) ∧ (𝜒 ∧ 𝜂)) ↔ (((𝜑 ∧ 𝜃) ∧ (𝜓 ∧ 𝜏)) ∧ (𝜒 ∧ 𝜂)))
8	3, 6, 7	3bitr4i 306	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂)) ↔ ((𝜑 ∧ 𝜃) ∧ (𝜓 ∧ 𝜏) ∧ (𝜒 ∧ 𝜂)))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∧ 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:  3an6  1475  poxp3  8152  elfzuzb  13562  fzadd2  13604  ptbasin  23785  iimulcl  25147  nb3grpr  29790  nb3grpr2  29791  txpconn  35761  paddasslem9  40660  paddasslem10  40661  gboge9  48587