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 ⊢ ( ⊤ → 𝜑 )
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 ⊢ ( 𝜓 → 𝜃 )