retbwax2 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > retbwax2		Structured version Visualization version Unicode version

Theorem retbwax2 1641

Description: tbw-ax2 1626 rederived from merco1 1638. (Contributed by Anthony Hart, 17-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

**Assertion**
Ref	Expression
retbwax2

**Proof of Theorem retbwax2**
Step	Hyp	Ref	Expression
1		merco1lem1 1639	. . . 4
2		merco1 1638	. . . 4
3	1, 2	ax-mp 5	. . 3
4		merco1 1638	. . . 4
5		merco1 1638	. . . 4
6	4, 5	ax-mp 5	. . 3
7	3, 6	ax-mp 5	. 2
8		merco1lem1 1639	. . . 4
9		merco1 1638	. . . 4
10	8, 9	ax-mp 5	. . 3
11		merco1 1638	. . . 4
12		merco1 1638	. . . 4
13	11, 12	ax-mp 5	. . 3
14	10, 13	ax-mp 5	. 2
15	7, 14	ax-mp 5	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

wfal 1488

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-tru 1486 df-fal 1489

This theorem is referenced by: merco1lem2 1642 merco1lem3 1643 retbwax3 1648

W3C validator