Theorem 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	$$⊢\left(\top \wedge \phi \right)\to \psi$$
Assertion	uunT1	$$⊢\phi \to \psi$$

Proof

Step	Hyp	Ref	Expression
1		uunT1.1	$$⊢\left(\top \wedge \phi \right)\to \psi$$
2		orc	$$⊢\phi \to \left(\phi \vee \neg \phi \right)$$
3		tru	$$⊢\top$$
4		biid	$$⊢\phi \leftrightarrow \phi$$
5	3 4	2th	$$⊢\top \leftrightarrow \left(\phi \leftrightarrow \phi \right)$$
6		exmid	$$⊢\left(\phi \vee \neg \phi \right)$$
7	6	a1i	$$⊢\left(\phi \leftrightarrow \phi \right)\to \left(\phi \vee \neg \phi \right)$$
8		biidd	$$⊢\left(\phi \vee \neg \phi \right)\to \left(\phi \leftrightarrow \phi \right)$$
9	7 8	impbii	$$⊢\left(\phi \leftrightarrow \phi \right)\leftrightarrow \left(\phi \vee \neg \phi \right)$$
10	5 9	bitri	$$⊢\top \leftrightarrow \left(\phi \vee \neg \phi \right)$$
11	2 10	sylibr	$$⊢\phi \to \top$$
12	11 1	mpancom	$$⊢\phi \to \psi$$