Metamath Proof Explorer


Theorem ee10an

Description: e10an without virtual deductions. sylancl is also e10an without virtual deductions, except the order of the hypotheses is different. (Contributed by Alan Sare, 25-Jul-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses ee10an.1
|- ( ph -> ps )
ee10an.2
|- ch
ee10an.3
|- ( ( ps /\ ch ) -> th )
Assertion ee10an
|- ( ph -> th )

Proof

Step Hyp Ref Expression
1 ee10an.1
 |-  ( ph -> ps )
2 ee10an.2
 |-  ch
3 ee10an.3
 |-  ( ( ps /\ ch ) -> th )
4 1 2 3 sylancl
 |-  ( ph -> th )