dalemkehl - Mathbox for Norm Megill

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

Theorem dalemkehl 33259

Description: Lemma for dath 33372. 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 1141	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
3	1, 2	sylbi 200	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 189 $/\$ wa 376 $/\$ w3a 1007

wcel 1904 class class class wbr 4395

cfv 5589 (class class class)co 6308

cbs 15199

chlt 32987

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 190 df-an 378 df-3an 1009

This theorem is referenced by: dalemkelat 33260 dalemkeop 33261 dalempjqeb 33281 dalemsjteb 33282 dalemtjueb 33283 dalemqrprot 33284 dalempnes 33287 dalemqnet 33288 dalempjsen 33289 dalemply 33290 dalemsly 33291 dalemswapyz 33292 dalemrot 33293 dalemrotyz 33294 dalem1 33295 dalemcea 33296 dalem2 33297 dalemdea 33298 dalem3 33300 dalem4 33301 dalem5 33303 dalem-cly 33307 dalem9 33308 dalem11 33310 dalem12 33311 dalem13 33312 dalem15 33314 dalem16 33315 dalem17 33316 dalem18 33317 dalem19 33318 dalemswapyzps 33326 dalemcjden 33328 dalem21 33330 dalem22 33331 dalem23 33332 dalem24 33333 dalem25 33334 dalem27 33335 dalem28 33336 dalem38 33346 dalem39 33347 dalem41 33349 dalem42 33350 dalem43 33351 dalem44 33352 dalem45 33353 dalem51 33359 dalem52 33360 dalem54 33362 dalem55 33363 dalem56 33364 dalem57 33365 dalem58 33366 dalem59 33367 dalem60 33368