dalemceb - Mathbox for Norm Megill

	Mathbox for Norm Megill	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > dalemceb		Structured version Unicode version

Theorem dalemceb 33601

Description: Lemma for dath 33699. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.)

**Hypotheses**
Ref	Expression
dalema.ph	$/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
dalema.a

**Assertion**
Ref	Expression
dalemceb

**Proof of Theorem dalemceb**
Step	Hyp	Ref	Expression
1		dalema.ph	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
2		simp11r 1100	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
3	1, 2	sylbi 195	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 369 $/\$ w3a 965

wceq 1370

wcel 1758 class class class wbr 4395

cfv 5521 (class class class)co 6195

cbs 14287

catm 33227

chlt 33314

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 185 df-an 371 df-3an 967

This theorem is referenced by: dalemcnes 33613 dalempnes 33614 dalemqnet 33615 dalemrot 33620 dalemcea 33623 dalem5 33630 dalem8 33633 dalem-cly 33634 dalem13 33639 dalem17 33643 dalem21 33657 dalem25 33661