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

Metamath Proof Explorer

Theorem un10

Description: A unionizing deduction. (Contributed by Alan Sare, 28-Apr-2015) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis un10.1 ⊢ (    (    𝜑    ,    ⊤    )    ▶    𝜓    )
Assertion un10 (    𝜑    ▶    𝜓    )

Proof

Step Hyp Ref Expression
1 un10.1 ⊢ (    (    𝜑    ,    ⊤    )    ▶    𝜓    )
2 tru ⊢ ⊤
3 2 jctr ⊢ ( 𝜑 → ( 𝜑 ∧ ⊤ ) )
4 1 dfvd2ani ⊢ ( ( 𝜑 ∧ ⊤ ) → 𝜓 )
5 3 4 syl ⊢ ( 𝜑 → 𝜓 )
6 5 dfvd1ir ⊢ (    𝜑    ▶    𝜓    )