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 ) ) ) |
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 ) ) ) |