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
|- ( ph -> ( ps \/ ( ch /\ th ) ) )
Assertion ex-natded5.7
|- ( ph -> ( ps \/ ch ) )

Proof

Step Hyp Ref Expression
1 ex-natded5.7.1
 |-  ( ph -> ( ps \/ ( ch /\ th ) ) )
2 simpr
 |-  ( ( ph /\ ps ) -> ps )
3 2 orcd
 |-  ( ( ph /\ ps ) -> ( ps \/ ch ) )
4 simpr
 |-  ( ( ph /\ ( ch /\ th ) ) -> ( ch /\ th ) )
5 4 simpld
 |-  ( ( ph /\ ( ch /\ th ) ) -> ch )
6 5 olcd
 |-  ( ( ph /\ ( ch /\ th ) ) -> ( ps \/ ch ) )
7 3 6 1 mpjaodan
 |-  ( ph -> ( ps \/ ch ) )