uunT1

Description: A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 3-Dec-2015) Proof was revised to accommodate a possible future version of df-tru . (Revised by David A. Wheeler, 8-May-2019) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	uunT1.1	$⊢ (⊤ \land φ) \to ψ$
	Assertion	uunT1	$⊢ φ \to ψ$

Proof

Step	Hyp	Ref	Expression
1		uunT1.1	$⊢ (⊤ \land φ) \to ψ$
2		orc	$⊢ φ \to (φ \lor \neg φ)$
3		tru	$⊢ ⊤$
4		biid	$⊢ φ \leftrightarrow φ$
5	3 4	2th	$⊢ ⊤ \leftrightarrow (φ \leftrightarrow φ)$
6		exmid	$⊢ (φ \lor \neg φ)$
7	6	a1i	$⊢ (φ \leftrightarrow φ) \to (φ \lor \neg φ)$
8		biidd	$⊢ (φ \lor \neg φ) \to (φ \leftrightarrow φ)$
9	7 8	impbii	$⊢ (φ \leftrightarrow φ) \leftrightarrow (φ \lor \neg φ)$
10	5 9	bitri	$⊢ ⊤ \leftrightarrow (φ \lor \neg φ)$
11	2 10	sylibr	$⊢ φ \to ⊤$
12	11 1	mpancom	$⊢ φ \to ψ$

Metamath Proof Explorer

Theorem uunT1

Proof