Description: Theorem 5.7 of Clemente p. 19, translated line by line using the interpretation of natural deduction in Metamath. A much more efficient proof, using more of Metamath and MPE's capabilities, is shown in ex-natded5.7-2 . 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 | 6 | ( ps \/ ( ch /\ th ) ) | ( ph -> ( ps \/ ( ch /\ th ) ) ) | Given | $e. No need for adantr because we do not move this into an ND hypothesis |
| 2 | 1 | ...| ps | ( ( ph /\ ps ) -> ps ) | ND hypothesis assumption (new scope) | simpr |
| 3 | 2 | ... ( ps \/ ch ) | ( ( ph /\ ps ) -> ( ps \/ ch ) ) | \/IL 2 | orcd , the MPE equivalent of \/IL, 1 |
| 4 | 3 | ...| ( ch /\ th ) | ( ( ph /\ ( ch /\ th ) ) -> ( ch /\ th ) ) | ND hypothesis assumption (new scope) | simpr |
| 5 | 4 | ... ch | ( ( ph /\ ( ch /\ th ) ) -> ch ) | /\EL 4 | simpld , the MPE equivalent of /\EL, 3 |
| 6 | 6 | ... ( ps \/ ch ) | ( ( ph /\ ( ch /\ th ) ) -> ( ps \/ ch ) ) | \/IR 5 | olcd , the MPE equivalent of \/IR, 4 |
| 7 | 7 | ( ps \/ ch ) | ( ph -> ( ps \/ ch ) ) | \/E 1,3,6 | mpjaodan , the MPE equivalent of \/E, 2,5,6 |
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 | ||
|---|---|---|---|
| Hypothesis | ex-natded5.7.1 | ⊢ ( 𝜑 → ( 𝜓 ∨ ( 𝜒 ∧ 𝜃 ) ) ) | |
| Assertion | ex-natded5.7 | ⊢ ( 𝜑 → ( 𝜓 ∨ 𝜒 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ex-natded5.7.1 | ⊢ ( 𝜑 → ( 𝜓 ∨ ( 𝜒 ∧ 𝜃 ) ) ) | |
| 2 | simpr | ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜓 ) | |
| 3 | 2 | orcd | ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝜓 ∨ 𝜒 ) ) |
| 4 | simpr | ⊢ ( ( 𝜑 ∧ ( 𝜒 ∧ 𝜃 ) ) → ( 𝜒 ∧ 𝜃 ) ) | |
| 5 | 4 | simpld | ⊢ ( ( 𝜑 ∧ ( 𝜒 ∧ 𝜃 ) ) → 𝜒 ) |
| 6 | 5 | olcd | ⊢ ( ( 𝜑 ∧ ( 𝜒 ∧ 𝜃 ) ) → ( 𝜓 ∨ 𝜒 ) ) |
| 7 | 3 6 1 | mpjaodan | ⊢ ( 𝜑 → ( 𝜓 ∨ 𝜒 ) ) |