Theorem prtlem70 39894

Description: Lemma for prter3 39919: a rearrangement of conjuncts. (Contributed by Rodolfo Medina, 20-Oct-2010.)

Assertion

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

Proof of Theorem prtlem70

Step	Hyp	Ref	Expression
1		anass 474	. . . 4 ⊢ ((((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜃)) ∧ (𝜒 ∧ 𝜏)) ↔ ((𝜑 ∧ 𝜓) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))))
2	1	anbi1i 636	. . 3 ⊢ (((((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜃)) ∧ (𝜒 ∧ 𝜏)) ∧ 𝜂) ↔ (((𝜑 ∧ 𝜓) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ∧ 𝜂))
3		anandi 689	. . . . 5 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜃)))
4	3	anbi1i 636	. . . 4 ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜃)) ∧ (𝜒 ∧ 𝜏)) ↔ (((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜃)) ∧ (𝜒 ∧ 𝜏)))
5	4	anbi1i 636	. . 3 ⊢ ((((𝜑 ∧ (𝜓 ∧ 𝜃)) ∧ (𝜒 ∧ 𝜏)) ∧ 𝜂) ↔ ((((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜃)) ∧ (𝜒 ∧ 𝜏)) ∧ 𝜂))
6		anass 474	. . . . 5 ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜂)) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ↔ (𝜑 ∧ ((𝜓 ∧ 𝜂) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏)))))
7		anass 474	. . . . . 6 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜂) ↔ (𝜑 ∧ (𝜓 ∧ 𝜂)))
8	7	anbi1i 636	. . . . 5 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜂) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ↔ ((𝜑 ∧ (𝜓 ∧ 𝜂)) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))))
9		ancom 466	. . . . 5 ⊢ ((((𝜓 ∧ 𝜂) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ∧ 𝜑) ↔ (𝜑 ∧ ((𝜓 ∧ 𝜂) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏)))))
10	6, 8, 9	3bitr4ri 307	. . . 4 ⊢ ((((𝜓 ∧ 𝜂) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ∧ 𝜑) ↔ (((𝜑 ∧ 𝜓) ∧ 𝜂) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))))
11		ancom 466	. . . . 5 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜂) ↔ (𝜂 ∧ (𝜑 ∧ 𝜓)))
12	11	anbi1i 636	. . . 4 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜂) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ↔ ((𝜂 ∧ (𝜑 ∧ 𝜓)) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))))
13		anass 474	. . . . 5 ⊢ (((𝜂 ∧ (𝜑 ∧ 𝜓)) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ↔ (𝜂 ∧ ((𝜑 ∧ 𝜓) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏)))))
14		ancom 466	. . . . 5 ⊢ ((𝜂 ∧ ((𝜑 ∧ 𝜓) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏)))) ↔ (((𝜑 ∧ 𝜓) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ∧ 𝜂))
15	13, 14	bitri 278	. . . 4 ⊢ (((𝜂 ∧ (𝜑 ∧ 𝜓)) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ↔ (((𝜑 ∧ 𝜓) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ∧ 𝜂))
16	10, 12, 15	3bitri 300	. . 3 ⊢ ((((𝜓 ∧ 𝜂) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ∧ 𝜑) ↔ (((𝜑 ∧ 𝜓) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ∧ 𝜂))
17	2, 5, 16	3bitr4ri 307	. 2 ⊢ ((((𝜓 ∧ 𝜂) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ∧ 𝜑) ↔ (((𝜑 ∧ (𝜓 ∧ 𝜃)) ∧ (𝜒 ∧ 𝜏)) ∧ 𝜂))
18		anass 474	. . 3 ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜃)) ∧ (𝜒 ∧ 𝜏)) ↔ (𝜑 ∧ ((𝜓 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))))
19	18	anbi1i 636	. 2 ⊢ ((((𝜑 ∧ (𝜓 ∧ 𝜃)) ∧ (𝜒 ∧ 𝜏)) ∧ 𝜂) ↔ ((𝜑 ∧ ((𝜓 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ∧ 𝜂))
20		an4 669	. . . . 5 ⊢ (((𝜓 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏)) ↔ ((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)))
21		anass 474	. . . . 5 ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) ↔ (𝜓 ∧ (𝜒 ∧ (𝜃 ∧ 𝜏))))
22	20, 21	bitri 278	. . . 4 ⊢ (((𝜓 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏)) ↔ (𝜓 ∧ (𝜒 ∧ (𝜃 ∧ 𝜏))))
23	22	anbi2i 635	. . 3 ⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ↔ (𝜑 ∧ (𝜓 ∧ (𝜒 ∧ (𝜃 ∧ 𝜏)))))
24	23	anbi1i 636	. 2 ⊢ (((𝜑 ∧ ((𝜓 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ∧ 𝜂) ↔ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ (𝜃 ∧ 𝜏)))) ∧ 𝜂))
25	17, 19, 24	3bitri 300	1 ⊢ ((((𝜓 ∧ 𝜂) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ∧ 𝜑) ↔ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ (𝜃 ∧ 𝜏)))) ∧ 𝜂))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401

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

This theorem is used by: (None)