Metamath Proof Explorer


Theorem uunT11p1

Description: A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis uunT11p1.1 ( ( 𝜑 ∧ ⊤ ∧ 𝜑 ) → 𝜓 )
Assertion uunT11p1 ( 𝜑𝜓 )

Proof

Step Hyp Ref Expression
1 uunT11p1.1 ( ( 𝜑 ∧ ⊤ ∧ 𝜑 ) → 𝜓 )
2 3anrot ( ( 𝜑 ∧ ⊤ ∧ 𝜑 ) ↔ ( ⊤ ∧ 𝜑𝜑 ) )
3 3anass ( ( ⊤ ∧ 𝜑𝜑 ) ↔ ( ⊤ ∧ ( 𝜑𝜑 ) ) )
4 truan ( ( ⊤ ∧ ( 𝜑𝜑 ) ) ↔ ( 𝜑𝜑 ) )
5 2 3 4 3bitri ( ( 𝜑 ∧ ⊤ ∧ 𝜑 ) ↔ ( 𝜑𝜑 ) )
6 anidm ( ( 𝜑𝜑 ) ↔ 𝜑 )
7 5 6 bitri ( ( 𝜑 ∧ ⊤ ∧ 𝜑 ) ↔ 𝜑 )
8 7 1 sylbir ( 𝜑𝜓 )