Description: A virtual deduction elimination rule (see syl3c ). (Contributed by Alan Sare, 14-Jun-2011) (Proof modification is discouraged.) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | e111.1 | |- (. ph ->. ps ). |
|
e111.2 | |- (. ph ->. ch ). |
||
e111.3 | |- (. ph ->. th ). |
||
e111.4 | |- ( ps -> ( ch -> ( th -> ta ) ) ) |
||
Assertion | e111 | |- (. ph ->. ta ). |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | e111.1 | |- (. ph ->. ps ). |
|
2 | e111.2 | |- (. ph ->. ch ). |
|
3 | e111.3 | |- (. ph ->. th ). |
|
4 | e111.4 | |- ( ps -> ( ch -> ( th -> ta ) ) ) |
|
5 | 3 | in1 | |- ( ph -> th ) |
6 | 1 | in1 | |- ( ph -> ps ) |
7 | 2 | in1 | |- ( ph -> ch ) |
8 | 6 7 4 | syl2im | |- ( ph -> ( ph -> ( th -> ta ) ) ) |
9 | 8 | pm2.43i | |- ( ph -> ( th -> ta ) ) |
10 | 5 9 | syl5com | |- ( ph -> ( ph -> ta ) ) |
11 | 10 | pm2.43i | |- ( ph -> ta ) |
12 | 11 | dfvd1ir | |- (. ph ->. ta ). |