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

Metamath Proof Explorer

Theorem el12

Description: Virtual deduction form of syl2an . (Contributed by Alan Sare, 23-Apr-2015) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses el12.1 ⊢ (    𝜑    ▶    𝜓    )
el12.2 ⊢ (    𝜏    ▶    𝜒    )
el12.3 ⊢ ( ( 𝜓 ∧ 𝜒 ) → 𝜃 )
Assertion el12 (    (    𝜑    ,    𝜏    )    ▶    𝜃    )

Proof

Step Hyp Ref Expression
1 el12.1 ⊢ (    𝜑    ▶    𝜓    )
2 el12.2 ⊢ (    𝜏    ▶    𝜒    )
3 el12.3 ⊢ ( ( 𝜓 ∧ 𝜒 ) → 𝜃 )
4 1 in1 ⊢ ( 𝜑 → 𝜓 )
5 2 in1 ⊢ ( 𝜏 → 𝜒 )
6 4 5 3 syl2an ⊢ ( ( 𝜑 ∧ 𝜏 ) → 𝜃 )
7 6 dfvd2anir ⊢ (    (    𝜑    ,    𝜏    )    ▶    𝜃    )