Theorem ex-natded5.3 27264

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 27265. A proof without context is shown in ex-natded5.3i 27266. 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 481 to move it into the ND hypothesis
2	5;6	( ch -> th )	( ph -> ( ch -> th ) )	Given	$e; adantr 481 to move it into the ND hypothesis
3	1	...| ps	( ( ph /\ ps ) -> ps )	ND hypothesis assumption	simpr 477, to access the new assumption
4	4	... ch	( ( ph /\ ps ) -> ch )	->E 1,3	mpd 15, the MPE equivalent of ->E, 1.3. adantr 481 was used to transform its dependency (we could also use imp 445 to get this directly from 1)
5	7	... th	( ( ph /\ ps ) -> th )	->E 2,4	mpd 15, the MPE equivalent of ->E, 4,6. adantr 481 was used to transform its dependency
6	8	... ( ch /\ th )	( ( ph /\ ps ) -> ( ch /\ th ) )	/\I 4,5	jca 554, the MPE equivalent of /\I, 4,7
7	9	( ps -> ( ch /\ th ) )	( ph -> ( ps -> ( ch /\ th ) ) )	->I 3,6	ex 450, 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.)

Hypotheses

Ref	Expression
ex-natded5.3.1	|- ( ph -> ( ps -> ch ) )
ex-natded5.3.2	|- ( ph -> ( ch -> th ) )

Assertion

Ref	Expression
ex-natded5.3	|- ( ph -> ( ps -> ( ch /\ th ) ) )

Proof of Theorem ex-natded5.3

Step	Hyp	Ref	Expression
1		simpr 477	. . . 4 |- ( ( ph /\ ps ) -> ps )
2		ex-natded5.3.1	. . . . 5 |- ( ph -> ( ps -> ch ) )
3	2	adantr 481	. . . 4 |- ( ( ph /\ ps ) -> ( ps -> ch ) )
4	1, 3	mpd 15	. . 3 |- ( ( ph /\ ps ) -> ch )
5		ex-natded5.3.2	. . . . 5 |- ( ph -> ( ch -> th ) )
6	5	adantr 481	. . . 4 |- ( ( ph /\ ps ) -> ( ch -> th ) )
7	4, 6	mpd 15	. . 3 |- ( ( ph /\ ps ) -> th )
8	4, 7	jca 554	. 2 |- ( ( ph /\ ps ) -> ( ch /\ th ) )
9	8	ex 450	1 |- ( ph -> ( ps -> ( ch /\ th ) ) )

Syntax hints:   -> wi 4   /\ wa 384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by: (None)