This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ ⊤ \to φ$
	uun0.1.2	$⊢ ψ \to χ$
	uun0.1.3	$⊢ (⊤ \land ψ) \to θ$
Assertion	uun0.1	$⊢ ψ \to θ$

Proof

Step	Hyp	Ref	Expression
1		uun0.1.1	$⊢ ⊤ \to φ$
2		uun0.1.2	$⊢ ψ \to χ$
3		uun0.1.3	$⊢ (⊤ \land ψ) \to θ$
4		tru	$⊢ ⊤$
5	1 2	pm3.2i	$⊢ ((⊤ \to φ) \land (ψ \to χ))$
6	5 3	pm3.2i	$⊢ (((⊤ \to φ) \land (ψ \to χ)) \land ((⊤ \land ψ) \to θ))$
7	6	simpri	$⊢ (⊤ \land ψ) \to θ$
8	7	ex	$⊢ ⊤ \to (ψ \to θ)$
9	4 8	ax-mp	$⊢ ψ \to θ$