Metamath Proof Explorer


Theorem eel0321old

Description: el0321old without virtual deductions. (Contributed by Alan Sare, 13-Jun-2015) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 eel0321old.1
 |-  ph
2 eel0321old.2
 |-  ( ( ps /\ ch /\ th ) -> ta )
3 eel0321old.3
 |-  ( ( ph /\ ta ) -> et )
4 1 2 3 sylancr
 |-  ( ( ps /\ ch /\ th ) -> et )