uun2221

Description: A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 30-Dec-2016) (Proof modification is discouraged.) (New usage is discouraged.) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	uun2221.1	$⊢ (φ \land φ \land (ψ \land φ)) \to χ$
	Assertion	uun2221	$⊢ (ψ \land φ) \to χ$

Proof

Step	Hyp	Ref	Expression
1		uun2221.1	$⊢ (φ \land φ \land (ψ \land φ)) \to χ$
2		3anass	$⊢ (φ \land φ \land (ψ \land φ)) \leftrightarrow (φ \land (φ \land (ψ \land φ)))$
3		anabs5	$⊢ (φ \land (φ \land (ψ \land φ))) \leftrightarrow (φ \land (ψ \land φ))$
4	2 3	bitri	$⊢ (φ \land φ \land (ψ \land φ)) \leftrightarrow (φ \land (ψ \land φ))$
5		ancom	$⊢ (φ \land ψ) \leftrightarrow (ψ \land φ)$
6	5	anbi2i	$⊢ (φ \land (φ \land ψ)) \leftrightarrow (φ \land (ψ \land φ))$
7	4 6	bitr4i	$⊢ (φ \land φ \land (ψ \land φ)) \leftrightarrow (φ \land (φ \land ψ))$
8		anabs5	$⊢ (φ \land (φ \land ψ)) \leftrightarrow (φ \land ψ)$
9	8 5	bitri	$⊢ (φ \land (φ \land ψ)) \leftrightarrow (ψ \land φ)$
10	7 9	bitri	$⊢ (φ \land φ \land (ψ \land φ)) \leftrightarrow (ψ \land φ)$
11	10	imbi1i	$⊢ ((φ \land φ \land (ψ \land φ)) \to χ) \leftrightarrow ((ψ \land φ) \to χ)$
12	1 11	mpbi	$⊢ (ψ \land φ) \to χ$

Metamath Proof Explorer

Theorem uun2221

Proof