Metamath Proof Explorer


Theorem ex-natded5.3

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 TranslationND Rationale MPE Rationale
12;3 ( ps -> ch ) ( ph -> ( ps -> ch ) ) Given $e; adantr to move it into the ND hypothesis
25;6 ( ch -> th ) ( ph -> ( ch -> th ) ) Given $e; adantr to move it into the ND hypothesis
31 ...| ps ( ( ph /\ ps ) -> ps ) ND hypothesis assumption simpr , to access the new assumption
44 ... 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)
57 ... th ( ( ph /\ ps ) -> th ) ->E 2,4 mpd , the MPE equivalent of ->E, 4,6. adantr was used to transform its dependency
68 ... ( ch /\ th ) ( ( ph /\ ps ) -> ( ch /\ th ) ) /\I 4,5 jca , the MPE equivalent of /\I, 4,7
79 ( 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 ) ) )

Proof

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 ) ) )