Description: exinst11 without virtual deductions. (Contributed by Alan Sare, 21-Apr-2013) (Proof modification is discouraged.) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | eexinst11.1 | |- ( ph -> E. x ps ) |
|
eexinst11.2 | |- ( ph -> ( ps -> ch ) ) |
||
eexinst11.3 | |- ( ph -> A. x ph ) |
||
eexinst11.4 | |- ( ch -> A. x ch ) |
||
Assertion | eexinst11 | |- ( ph -> ch ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eexinst11.1 | |- ( ph -> E. x ps ) |
|
2 | eexinst11.2 | |- ( ph -> ( ps -> ch ) ) |
|
3 | eexinst11.3 | |- ( ph -> A. x ph ) |
|
4 | eexinst11.4 | |- ( ch -> A. x ch ) |
|
5 | 3 4 2 | exlimdh | |- ( ph -> ( E. x ps -> ch ) ) |
6 | 1 5 | syl5com | |- ( ph -> ( ph -> ch ) ) |
7 | 6 | pm2.43i | |- ( ph -> ch ) |