Theorem prtlem70 35995

Description: Lemma for prter3 36020: 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 471	. . . 4 ⊢ ((((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜃)) ∧ (𝜒 ∧ 𝜏)) ↔ ((𝜑 ∧ 𝜓) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))))
2	1	anbi1i 625	. . 3 ⊢ (((((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜃)) ∧ (𝜒 ∧ 𝜏)) ∧ 𝜂) ↔ (((𝜑 ∧ 𝜓) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ∧ 𝜂))
3		anandi 674	. . . . 5 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜃)))
4	3	anbi1i 625	. . . 4 ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜃)) ∧ (𝜒 ∧ 𝜏)) ↔ (((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜃)) ∧ (𝜒 ∧ 𝜏)))
5	4	anbi1i 625	. . 3 ⊢ ((((𝜑 ∧ (𝜓 ∧ 𝜃)) ∧ (𝜒 ∧ 𝜏)) ∧ 𝜂) ↔ ((((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜃)) ∧ (𝜒 ∧ 𝜏)) ∧ 𝜂))
6		anass 471	. . . . 5 ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜂)) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ↔ (𝜑 ∧ ((𝜓 ∧ 𝜂) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏)))))
7		anass 471	. . . . . 6 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜂) ↔ (𝜑 ∧ (𝜓 ∧ 𝜂)))
8	7	anbi1i 625	. . . . 5 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜂) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ↔ ((𝜑 ∧ (𝜓 ∧ 𝜂)) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))))
9		ancom 463	. . . . 5 ⊢ ((((𝜓 ∧ 𝜂) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ∧ 𝜑) ↔ (𝜑 ∧ ((𝜓 ∧ 𝜂) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏)))))
10	6, 8, 9	3bitr4ri 306	. . . 4 ⊢ ((((𝜓 ∧ 𝜂) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ∧ 𝜑) ↔ (((𝜑 ∧ 𝜓) ∧ 𝜂) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))))
11		ancom 463	. . . . 5 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜂) ↔ (𝜂 ∧ (𝜑 ∧ 𝜓)))
12	11	anbi1i 625	. . . 4 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜂) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ↔ ((𝜂 ∧ (𝜑 ∧ 𝜓)) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))))
13		anass 471	. . . . 5 ⊢ (((𝜂 ∧ (𝜑 ∧ 𝜓)) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ↔ (𝜂 ∧ ((𝜑 ∧ 𝜓) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏)))))
14		ancom 463	. . . . 5 ⊢ ((𝜂 ∧ ((𝜑 ∧ 𝜓) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏)))) ↔ (((𝜑 ∧ 𝜓) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ∧ 𝜂))
15	13, 14	bitri 277	. . . 4 ⊢ (((𝜂 ∧ (𝜑 ∧ 𝜓)) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ↔ (((𝜑 ∧ 𝜓) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ∧ 𝜂))
16	10, 12, 15	3bitri 299	. . 3 ⊢ ((((𝜓 ∧ 𝜂) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ∧ 𝜑) ↔ (((𝜑 ∧ 𝜓) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ∧ 𝜂))
17	2, 5, 16	3bitr4ri 306	. 2 ⊢ ((((𝜓 ∧ 𝜂) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ∧ 𝜑) ↔ (((𝜑 ∧ (𝜓 ∧ 𝜃)) ∧ (𝜒 ∧ 𝜏)) ∧ 𝜂))
18		anass 471	. . 3 ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜃)) ∧ (𝜒 ∧ 𝜏)) ↔ (𝜑 ∧ ((𝜓 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))))
19	18	anbi1i 625	. 2 ⊢ ((((𝜑 ∧ (𝜓 ∧ 𝜃)) ∧ (𝜒 ∧ 𝜏)) ∧ 𝜂) ↔ ((𝜑 ∧ ((𝜓 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ∧ 𝜂))
20		an4 654	. . . . 5 ⊢ (((𝜓 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏)) ↔ ((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)))
21		anass 471	. . . . 5 ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) ↔ (𝜓 ∧ (𝜒 ∧ (𝜃 ∧ 𝜏))))
22	20, 21	bitri 277	. . . 4 ⊢ (((𝜓 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏)) ↔ (𝜓 ∧ (𝜒 ∧ (𝜃 ∧ 𝜏))))
23	22	anbi2i 624	. . 3 ⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ↔ (𝜑 ∧ (𝜓 ∧ (𝜒 ∧ (𝜃 ∧ 𝜏)))))
24	23	anbi1i 625	. 2 ⊢ (((𝜑 ∧ ((𝜓 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ∧ 𝜂) ↔ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ (𝜃 ∧ 𝜏)))) ∧ 𝜂))
25	17, 19, 24	3bitri 299	1 ⊢ ((((𝜓 ∧ 𝜂) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ∧ 𝜑) ↔ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ (𝜃 ∧ 𝜏)))) ∧ 𝜂))

Syntax hints:   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by: (None)