Description: An elimination deduction. (Contributed by Alan Sare, 17-Oct-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | mpsyl4anc.1 | |- ph |
|
mpsyl4anc.2 | |- ps |
||
mpsyl4anc.3 | |- ch |
||
mpsyl4anc.4 | |- ( th -> ta ) |
||
mpsyl4anc.5 | |- ( ( ( ( ph /\ ps ) /\ ch ) /\ ta ) -> et ) |
||
Assertion | mpsyl4anc | |- ( th -> et ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpsyl4anc.1 | |- ph |
|
2 | mpsyl4anc.2 | |- ps |
|
3 | mpsyl4anc.3 | |- ch |
|
4 | mpsyl4anc.4 | |- ( th -> ta ) |
|
5 | mpsyl4anc.5 | |- ( ( ( ( ph /\ ps ) /\ ch ) /\ ta ) -> et ) |
|
6 | 1 | a1i | |- ( th -> ph ) |
7 | 2 | a1i | |- ( th -> ps ) |
8 | 3 | a1i | |- ( th -> ch ) |
9 | 6 7 8 4 5 | syl1111anc | |- ( th -> et ) |