hbimpg - Mathbox for Alan Sare

	Mathbox for Alan Sare		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > hbimpg		Structured version Visualization version Unicode version

Theorem hbimpg 38770

Description: A closed form of hbim 2127. Derived from hbimpgVD 39140. (Contributed by Alan Sare, 8-Feb-2014.) (Proof modification is discouraged.) (New usage is discouraged.)

**Assertion**
Ref	Expression
hbimpg	$/\$

**Proof of Theorem hbimpg**
Step	Hyp	Ref	Expression
1		hba1 2151	. . 3
2		hba1 2151	. . 3
3	1, 2	hban 2128	. 2 $/\$ $/\$
4		hbntal 38769	. . . . . 6
5	4	adantr 481	. . . . 5 $/\$
6	5	19.21bi 2059	. . . 4 $/\$
7		pm2.21 120	. . . . 5
8	7	alimi 1739	. . . 4
9	6, 8	syl6 35	. . 3 $/\$
10		simpr 477	. . . . 5 $/\$
11	10	19.21bi 2059	. . . 4 $/\$
12		ax-1 6	. . . . 5
13	12	alimi 1739	. . . 4
14	11, 13	syl6 35	. . 3 $/\$
15	9, 14	jad 174	. 2 $/\$
16	3, 15	alrimih 1751	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4 $/\$ wa 384

wal 1481

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-10 2019 ax-12 2047

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710

This theorem is referenced by: (None)

W3C validator