Metamath Proof Explorer


Theorem ee11an

Description: e11an without virtual deductions. syl22anc is also e11an without virtual deductions, exept with a different order of hypotheses. (Contributed by Alan Sare, 8-Jul-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses ee11an.1 ( 𝜑𝜓 )
ee11an.2 ( 𝜑𝜒 )
ee11an.3 ( ( 𝜓𝜒 ) → 𝜃 )
Assertion ee11an ( 𝜑𝜃 )

Proof

Step Hyp Ref Expression
1 ee11an.1 ( 𝜑𝜓 )
2 ee11an.2 ( 𝜑𝜒 )
3 ee11an.3 ( ( 𝜓𝜒 ) → 𝜃 )
4 3 ex ( 𝜓 → ( 𝜒𝜃 ) )
5 1 2 4 sylc ( 𝜑𝜃 )