prtlem70

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

		Ref	Expression
	Assertion	prtlem70	$⊢ (((ψ \land η) \land ((φ \land θ) \land (χ \land τ))) \land φ) \leftrightarrow ((φ \land (ψ \land (χ \land (θ \land τ)))) \land η)$

Proof

Step	Hyp	Ref	Expression
1		anass	$⊢ (((φ \land ψ) \land (φ \land θ)) \land (χ \land τ)) \leftrightarrow ((φ \land ψ) \land ((φ \land θ) \land (χ \land τ)))$
2	1	anbi1i	$⊢ ((((φ \land ψ) \land (φ \land θ)) \land (χ \land τ)) \land η) \leftrightarrow (((φ \land ψ) \land ((φ \land θ) \land (χ \land τ))) \land η)$
3		anandi	$⊢ (φ \land (ψ \land θ)) \leftrightarrow ((φ \land ψ) \land (φ \land θ))$
4	3	anbi1i	$⊢ ((φ \land (ψ \land θ)) \land (χ \land τ)) \leftrightarrow (((φ \land ψ) \land (φ \land θ)) \land (χ \land τ))$
5	4	anbi1i	$⊢ (((φ \land (ψ \land θ)) \land (χ \land τ)) \land η) \leftrightarrow ((((φ \land ψ) \land (φ \land θ)) \land (χ \land τ)) \land η)$
6		anass	$⊢ ((φ \land (ψ \land η)) \land ((φ \land θ) \land (χ \land τ))) \leftrightarrow (φ \land ((ψ \land η) \land ((φ \land θ) \land (χ \land τ))))$
7		anass	$⊢ ((φ \land ψ) \land η) \leftrightarrow (φ \land (ψ \land η))$
8	7	anbi1i	$⊢ (((φ \land ψ) \land η) \land ((φ \land θ) \land (χ \land τ))) \leftrightarrow ((φ \land (ψ \land η)) \land ((φ \land θ) \land (χ \land τ)))$
9		ancom	$⊢ (((ψ \land η) \land ((φ \land θ) \land (χ \land τ))) \land φ) \leftrightarrow (φ \land ((ψ \land η) \land ((φ \land θ) \land (χ \land τ))))$
10	6 8 9	3bitr4ri	$⊢ (((ψ \land η) \land ((φ \land θ) \land (χ \land τ))) \land φ) \leftrightarrow (((φ \land ψ) \land η) \land ((φ \land θ) \land (χ \land τ)))$
11		ancom	$⊢ ((φ \land ψ) \land η) \leftrightarrow (η \land (φ \land ψ))$
12	11	anbi1i	$⊢ (((φ \land ψ) \land η) \land ((φ \land θ) \land (χ \land τ))) \leftrightarrow ((η \land (φ \land ψ)) \land ((φ \land θ) \land (χ \land τ)))$
13		anass	$⊢ ((η \land (φ \land ψ)) \land ((φ \land θ) \land (χ \land τ))) \leftrightarrow (η \land ((φ \land ψ) \land ((φ \land θ) \land (χ \land τ))))$
14		ancom	$⊢ (η \land ((φ \land ψ) \land ((φ \land θ) \land (χ \land τ)))) \leftrightarrow (((φ \land ψ) \land ((φ \land θ) \land (χ \land τ))) \land η)$
15	13 14	bitri	$⊢ ((η \land (φ \land ψ)) \land ((φ \land θ) \land (χ \land τ))) \leftrightarrow (((φ \land ψ) \land ((φ \land θ) \land (χ \land τ))) \land η)$
16	10 12 15	3bitri	$⊢ (((ψ \land η) \land ((φ \land θ) \land (χ \land τ))) \land φ) \leftrightarrow (((φ \land ψ) \land ((φ \land θ) \land (χ \land τ))) \land η)$
17	2 5 16	3bitr4ri	$⊢ (((ψ \land η) \land ((φ \land θ) \land (χ \land τ))) \land φ) \leftrightarrow (((φ \land (ψ \land θ)) \land (χ \land τ)) \land η)$
18		anass	$⊢ ((φ \land (ψ \land θ)) \land (χ \land τ)) \leftrightarrow (φ \land ((ψ \land θ) \land (χ \land τ)))$
19	18	anbi1i	$⊢ (((φ \land (ψ \land θ)) \land (χ \land τ)) \land η) \leftrightarrow ((φ \land ((ψ \land θ) \land (χ \land τ))) \land η)$
20		an4	$⊢ ((ψ \land θ) \land (χ \land τ)) \leftrightarrow ((ψ \land χ) \land (θ \land τ))$
21		anass	$⊢ ((ψ \land χ) \land (θ \land τ)) \leftrightarrow (ψ \land (χ \land (θ \land τ)))$
22	20 21	bitri	$⊢ ((ψ \land θ) \land (χ \land τ)) \leftrightarrow (ψ \land (χ \land (θ \land τ)))$
23	22	anbi2i	$⊢ (φ \land ((ψ \land θ) \land (χ \land τ))) \leftrightarrow (φ \land (ψ \land (χ \land (θ \land τ))))$
24	23	anbi1i	$⊢ ((φ \land ((ψ \land θ) \land (χ \land τ))) \land η) \leftrightarrow ((φ \land (ψ \land (χ \land (θ \land τ)))) \land η)$
25	17 19 24	3bitri	$⊢ (((ψ \land η) \land ((φ \land θ) \land (χ \land τ))) \land φ) \leftrightarrow ((φ \land (ψ \land (χ \land (θ \land τ)))) \land η)$

Metamath Proof Explorer

Theorem prtlem70

Proof