Metamath Proof Explorer


Theorem ee13

Description: e13 without virtual deduction connectives. Special theorem needed for the Virtual Deduction translation tool. (Contributed by Alan Sare, 28-Oct-2011) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 ee13.1
 |-  ( ph -> ps )
2 ee13.2
 |-  ( ph -> ( ch -> ( th -> ta ) ) )
3 ee13.3
 |-  ( ps -> ( ta -> et ) )
4 1 3 syl
 |-  ( ph -> ( ta -> et ) )
5 2 4 syl6d
 |-  ( ph -> ( ch -> ( th -> et ) ) )