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 34434

Description: Lemma for dath 34532. 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 1108	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
3	1, 2	sylbi 195	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1379

wcel 1767 class class class wbr 4447

cfv 5586 (class class class)co 6282

cbs 14486

catm 34060

chlt 34147

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 975

This theorem is referenced by: dalemcnes 34446 dalempnes 34447 dalemqnet 34448 dalemrot 34453 dalemcea 34456 dalem5 34463 dalem8 34466 dalem-cly 34467 dalem13 34472 dalem17 34476 dalem21 34490 dalem25 34494