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 33606

Description: Lemma for dath 33719. 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 1099	. 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

wcel 1758 class class class wbr 4401

cfv 5527 (class class class)co 6201

cbs 14293

chlt 33334

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: dalemkelat 33607 dalemkeop 33608 dalempjqeb 33628 dalemsjteb 33629 dalemtjueb 33630 dalemqrprot 33631 dalempnes 33634 dalemqnet 33635 dalempjsen 33636 dalemply 33637 dalemsly 33638 dalemswapyz 33639 dalemrot 33640 dalemrotyz 33641 dalem1 33642 dalemcea 33643 dalem2 33644 dalemdea 33645 dalem3 33647 dalem4 33648 dalem5 33650 dalem-cly 33654 dalem9 33655 dalem11 33657 dalem12 33658 dalem13 33659 dalem15 33661 dalem16 33662 dalem17 33663 dalem18 33664 dalem19 33665 dalemswapyzps 33673 dalemcjden 33675 dalem21 33677 dalem22 33678 dalem23 33679 dalem24 33680 dalem25 33681 dalem27 33682 dalem28 33683 dalem38 33693 dalem39 33694 dalem41 33696 dalem42 33697 dalem43 33698 dalem44 33699 dalem45 33700 dalem51 33706 dalem52 33707 dalem54 33709 dalem55 33710 dalem56 33711 dalem57 33712 dalem58 33713 dalem59 33714 dalem60 33715