Metamath Proof Explorer

Theorem ex-natded5.7

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 TranslationND Rationale MPE Rationale
16 ( ps \/ ( ch /\ th ) ) ( ph -> ( ps \/ ( ch /\ th ) ) ) Given $e. No need for adantr because we do not move this into an ND hypothesis
21 ...| ps ( ( ph /\ ps ) -> ps ) ND hypothesis assumption (new scope) simpr
32 ... ( ps \/ ch ) ( ( ph /\ ps ) -> ( ps \/ ch ) ) \/IL 2 orcd , the MPE equivalent of \/IL, 1
43 ...| ( ch /\ th ) ( ( ph /\ ( ch /\ th ) ) -> ( ch /\ th ) ) ND hypothesis assumption (new scope) simpr
54 ... ch ( ( ph /\ ( ch /\ th ) ) -> ch ) /\EL 4 simpld , the MPE equivalent of /\EL, 3
66 ... ( ps \/ ch ) ( ( ph /\ ( ch /\ th ) ) -> ( ps \/ ch ) ) \/IR 5 olcd , the MPE equivalent of \/IR, 4
77 ( 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 ⊢ φ → ψ ∨ χ

Proof

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 ⊢ φ → ψ ∨ χ