Theorem uun0.1

Description: Convention notation form of un0.1 . (Contributed by Alan Sare, 23-Apr-2015) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	uun0.1.1	|- ( T. -> ph )
	uun0.1.2	|- ( ps -> ch )
	uun0.1.3	|- ( ( T. /\ ps ) -> th )
Assertion	uun0.1	|- ( ps -> th )

Proof

Step	Hyp	Ref	Expression
1		uun0.1.1	|- ( T. -> ph )
2		uun0.1.2	|- ( ps -> ch )
3		uun0.1.3	|- ( ( T. /\ ps ) -> th )
4		tru	|- T.
5	1 2	pm3.2i	|- ( ( T. -> ph ) /\ ( ps -> ch ) )
6	5 3	pm3.2i	|- ( ( ( T. -> ph ) /\ ( ps -> ch ) ) /\ ( ( T. /\ ps ) -> th ) )
7	6	simpri	|- ( ( T. /\ ps ) -> th )
8	7	ex	|- ( T. -> ( ps -> th ) )
9	4 8	ax-mp	|- ( ps -> th )