Theorem prtlem70 33157

Description: Lemma for prter3 33185: 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 679	. . . 4 ⊢ ((((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜃)) ∧ (𝜒 ∧ 𝜏)) ↔ ((𝜑 ∧ 𝜓) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))))
2	1	anbi1i 727	. . 3 ⊢ (((((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜃)) ∧ (𝜒 ∧ 𝜏)) ∧ 𝜂) ↔ (((𝜑 ∧ 𝜓) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ∧ 𝜂))
3		anandi 867	. . . . 5 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜃)))
4	3	anbi1i 727	. . . 4 ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜃)) ∧ (𝜒 ∧ 𝜏)) ↔ (((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜃)) ∧ (𝜒 ∧ 𝜏)))
5	4	anbi1i 727	. . 3 ⊢ ((((𝜑 ∧ (𝜓 ∧ 𝜃)) ∧ (𝜒 ∧ 𝜏)) ∧ 𝜂) ↔ ((((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜃)) ∧ (𝜒 ∧ 𝜏)) ∧ 𝜂))
6		anass 679	. . . . 5 ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜂)) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ↔ (𝜑 ∧ ((𝜓 ∧ 𝜂) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏)))))
7		anass 679	. . . . . 6 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜂) ↔ (𝜑 ∧ (𝜓 ∧ 𝜂)))
8	7	anbi1i 727	. . . . 5 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜂) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ↔ ((𝜑 ∧ (𝜓 ∧ 𝜂)) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))))
9		ancom 465	. . . . 5 ⊢ ((((𝜓 ∧ 𝜂) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ∧ 𝜑) ↔ (𝜑 ∧ ((𝜓 ∧ 𝜂) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏)))))
10	6, 8, 9	3bitr4ri 292	. . . 4 ⊢ ((((𝜓 ∧ 𝜂) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ∧ 𝜑) ↔ (((𝜑 ∧ 𝜓) ∧ 𝜂) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))))
11		ancom 465	. . . . 5 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜂) ↔ (𝜂 ∧ (𝜑 ∧ 𝜓)))
12	11	anbi1i 727	. . . 4 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜂) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ↔ ((𝜂 ∧ (𝜑 ∧ 𝜓)) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))))
13		anass 679	. . . . 5 ⊢ (((𝜂 ∧ (𝜑 ∧ 𝜓)) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ↔ (𝜂 ∧ ((𝜑 ∧ 𝜓) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏)))))
14		ancom 465	. . . . 5 ⊢ ((𝜂 ∧ ((𝜑 ∧ 𝜓) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏)))) ↔ (((𝜑 ∧ 𝜓) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ∧ 𝜂))
15	13, 14	bitri 263	. . . 4 ⊢ (((𝜂 ∧ (𝜑 ∧ 𝜓)) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ↔ (((𝜑 ∧ 𝜓) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ∧ 𝜂))
16	10, 12, 15	3bitri 285	. . 3 ⊢ ((((𝜓 ∧ 𝜂) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ∧ 𝜑) ↔ (((𝜑 ∧ 𝜓) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ∧ 𝜂))
17	2, 5, 16	3bitr4ri 292	. 2 ⊢ ((((𝜓 ∧ 𝜂) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ∧ 𝜑) ↔ (((𝜑 ∧ (𝜓 ∧ 𝜃)) ∧ (𝜒 ∧ 𝜏)) ∧ 𝜂))
18		anass 679	. . 3 ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜃)) ∧ (𝜒 ∧ 𝜏)) ↔ (𝜑 ∧ ((𝜓 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))))
19	18	anbi1i 727	. 2 ⊢ ((((𝜑 ∧ (𝜓 ∧ 𝜃)) ∧ (𝜒 ∧ 𝜏)) ∧ 𝜂) ↔ ((𝜑 ∧ ((𝜓 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ∧ 𝜂))
20		an4 861	. . . . 5 ⊢ (((𝜓 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏)) ↔ ((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)))
21		anass 679	. . . . 5 ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) ↔ (𝜓 ∧ (𝜒 ∧ (𝜃 ∧ 𝜏))))
22	20, 21	bitri 263	. . . 4 ⊢ (((𝜓 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏)) ↔ (𝜓 ∧ (𝜒 ∧ (𝜃 ∧ 𝜏))))
23	22	anbi2i 726	. . 3 ⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ↔ (𝜑 ∧ (𝜓 ∧ (𝜒 ∧ (𝜃 ∧ 𝜏)))))
24	23	anbi1i 727	. 2 ⊢ (((𝜑 ∧ ((𝜓 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ∧ 𝜂) ↔ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ (𝜃 ∧ 𝜏)))) ∧ 𝜂))
25	17, 19, 24	3bitri 285	1 ⊢ ((((𝜓 ∧ 𝜂) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ∧ 𝜑) ↔ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ (𝜃 ∧ 𝜏)))) ∧ 𝜂))

Syntax hints:   ↔ wb 195   ∧ wa 383

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 196  df-an 385

This theorem is referenced by: (None)