Description: Theorem 5.3 of Clemente p. 16, translated line by line using an interpretation of natural deduction in Metamath. A much more efficient proof, using more of Metamath and MPE's capabilities, is shown in ex-natded5.3-2 . A proof without context is shown in ex-natded5.3i . For information about ND and Metamath, see the page on Deduction Form and Natural Deduction in Metamath Proof Explorer. The original proof, which uses Fitch style, was written as follows:
| # | MPE# | ND Expression | MPE Translation | ND Rationale | MPE Rationale |
|---|---|---|---|---|---|
| 1 | 2;3 | ( ps -> ch ) | ( ph -> ( ps -> ch ) ) | Given | $e; adantr to move it into the ND hypothesis |
| 2 | 5;6 | ( ch -> th ) | ( ph -> ( ch -> th ) ) | Given | $e; adantr to move it into the ND hypothesis |
| 3 | 1 | ...| ps | ( ( ph /\ ps ) -> ps ) | ND hypothesis assumption | simpr , to access the new assumption |
| 4 | 4 | ... ch | ( ( ph /\ ps ) -> ch ) | ->E 1,3 | mpd , the MPE equivalent of ->E, 1.3. adantr was used to transform its dependency (we could also use imp to get this directly from 1) |
| 5 | 7 | ... th | ( ( ph /\ ps ) -> th ) | ->E 2,4 | mpd , the MPE equivalent of ->E, 4,6. adantr was used to transform its dependency |
| 6 | 8 | ... ( ch /\ th ) | ( ( ph /\ ps ) -> ( ch /\ th ) ) | /\I 4,5 | jca , the MPE equivalent of /\I, 4,7 |
| 7 | 9 | ( ps -> ( ch /\ th ) ) | ( ph -> ( ps -> ( ch /\ th ) ) ) | ->I 3,6 | ex , the MPE equivalent of ->I, 8 |
The original used Latin letters for predicates; we have replaced them with Greek letters to follow Metamath naming conventions and so that it is easier to follow the Metamath translation. The Metamath line-for-line translation of this natural deduction approach precedes every line with an antecedent including ph and uses the Metamath equivalents of the natural deduction rules. (Contributed by Mario Carneiro, 9-Feb-2017) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | ex-natded5.3.1 | |- ( ph -> ( ps -> ch ) ) |
|
| ex-natded5.3.2 | |- ( ph -> ( ch -> th ) ) |
||
| Assertion | ex-natded5.3 | |- ( ph -> ( ps -> ( ch /\ th ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ex-natded5.3.1 | |- ( ph -> ( ps -> ch ) ) |
|
| 2 | ex-natded5.3.2 | |- ( ph -> ( ch -> th ) ) |
|
| 3 | simpr | |- ( ( ph /\ ps ) -> ps ) |
|
| 4 | 1 | adantr | |- ( ( ph /\ ps ) -> ( ps -> ch ) ) |
| 5 | 3 4 | mpd | |- ( ( ph /\ ps ) -> ch ) |
| 6 | 2 | adantr | |- ( ( ph /\ ps ) -> ( ch -> th ) ) |
| 7 | 5 6 | mpd | |- ( ( ph /\ ps ) -> th ) |
| 8 | 5 7 | jca | |- ( ( ph /\ ps ) -> ( ch /\ th ) ) |
| 9 | 8 | ex | |- ( ph -> ( ps -> ( ch /\ th ) ) ) |