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	$$⊢\left(\phi \to \psi \right)$$
	el12.2	$$⊢\left(\tau \to \chi \right)$$
	el12.3	$$⊢\left(\psi \wedge \chi \right)\to \theta$$
Assertion	el12	$$⊢\left(\left(\phi ,\tau \right)\to \theta \right)$$

Proof

Step	Hyp	Ref	Expression
1		el12.1	$$⊢\left(\phi \to \psi \right)$$
2		el12.2	$$⊢\left(\tau \to \chi \right)$$
3		el12.3	$$⊢\left(\psi \wedge \chi \right)\to \theta$$
4	1	in1	$$⊢\phi \to \psi$$
5	2	in1	$$⊢\tau \to \chi$$
6	4 5 3	syl2an	$$⊢\left(\phi \wedge \tau \right)\to \theta$$
7	6	dfvd2anir	$$⊢\left(\left(\phi ,\tau \right)\to \theta \right)$$