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	⊢ (    (    𝜑    ,    𝜏    )    ▶    𝜃    )