Description: A virtual deduction elimination rule. (Contributed by Alan Sare, 13-Jun-2015) (Proof modification is discouraged.) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | el021old.1 | |- ph |
|
el021old.2 | |- (. (. ps ,. ch ). ->. th ). |
||
el021old.3 | |- ( ( ph /\ th ) -> ta ) |
||
Assertion | el021old | |- (. (. ps ,. ch ). ->. ta ). |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | el021old.1 | |- ph |
|
2 | el021old.2 | |- (. (. ps ,. ch ). ->. th ). |
|
3 | el021old.3 | |- ( ( ph /\ th ) -> ta ) |
|
4 | 2 | dfvd2ani | |- ( ( ps /\ ch ) -> th ) |
5 | 1 4 3 | sylancr | |- ( ( ps /\ ch ) -> ta ) |
6 | 5 | dfvd2anir | |- (. (. ps ,. ch ). ->. ta ). |