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	⊢ ( ⊤ → 𝜑 )
	uun0.1.2	⊢ ( 𝜓 → 𝜒 )
	uun0.1.3	⊢ ( ( ⊤ ∧ 𝜓 ) → 𝜃 )
Assertion	uun0.1	⊢ ( 𝜓 → 𝜃 )

Proof

Step	Hyp	Ref	Expression
1		uun0.1.1	⊢ ( ⊤ → 𝜑 )
2		uun0.1.2	⊢ ( 𝜓 → 𝜒 )
3		uun0.1.3	⊢ ( ( ⊤ ∧ 𝜓 ) → 𝜃 )
4		tru	⊢ ⊤
5	1 2	pm3.2i	⊢ ( ( ⊤ → 𝜑 ) ∧ ( 𝜓 → 𝜒 ) )
6	5 3	pm3.2i	⊢ ( ( ( ⊤ → 𝜑 ) ∧ ( 𝜓 → 𝜒 ) ) ∧ ( ( ⊤ ∧ 𝜓 ) → 𝜃 ) )
7	6	simpri	⊢ ( ( ⊤ ∧ 𝜓 ) → 𝜃 )
8	7	ex	⊢ ( ⊤ → ( 𝜓 → 𝜃 ) )
9	4 8	ax-mp	⊢ ( 𝜓 → 𝜃 )