dalemkehl - Mathbox for Norm Megill

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

Theorem dalemkehl 34294

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

**Hypothesis**
Ref	Expression
dalema.ph	$/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$

**Assertion**
Ref	Expression
dalemkehl

**Proof of Theorem dalemkehl**
Step	Hyp	Ref	Expression
1		dalema.ph	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
2		simp11l 1102	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
3	1, 2	sylbi 195	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wcel 1762 class class class wbr 4440

cfv 5579 (class class class)co 6275

cbs 14479

chlt 34022

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 970

This theorem is referenced by: dalemkelat 34295 dalemkeop 34296 dalempjqeb 34316 dalemsjteb 34317 dalemtjueb 34318 dalemqrprot 34319 dalempnes 34322 dalemqnet 34323 dalempjsen 34324 dalemply 34325 dalemsly 34326 dalemswapyz 34327 dalemrot 34328 dalemrotyz 34329 dalem1 34330 dalemcea 34331 dalem2 34332 dalemdea 34333 dalem3 34335 dalem4 34336 dalem5 34338 dalem-cly 34342 dalem9 34343 dalem11 34345 dalem12 34346 dalem13 34347 dalem15 34349 dalem16 34350 dalem17 34351 dalem18 34352 dalem19 34353 dalemswapyzps 34361 dalemcjden 34363 dalem21 34365 dalem22 34366 dalem23 34367 dalem24 34368 dalem25 34369 dalem27 34370 dalem28 34371 dalem38 34381 dalem39 34382 dalem41 34384 dalem42 34385 dalem43 34386 dalem44 34387 dalem45 34388 dalem51 34394 dalem52 34395 dalem54 34397 dalem55 34398 dalem56 34399 dalem57 34400 dalem58 34401 dalem59 34402 dalem60 34403