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 35760

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

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 367 $/\$ w3a 971

wcel 1826 class class class wbr 4367

cfv 5496 (class class class)co 6196

cbs 14634

chlt 35488

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 369 df-3an 973

This theorem is referenced by: dalemkelat 35761 dalemkeop 35762 dalempjqeb 35782 dalemsjteb 35783 dalemtjueb 35784 dalemqrprot 35785 dalempnes 35788 dalemqnet 35789 dalempjsen 35790 dalemply 35791 dalemsly 35792 dalemswapyz 35793 dalemrot 35794 dalemrotyz 35795 dalem1 35796 dalemcea 35797 dalem2 35798 dalemdea 35799 dalem3 35801 dalem4 35802 dalem5 35804 dalem-cly 35808 dalem9 35809 dalem11 35811 dalem12 35812 dalem13 35813 dalem15 35815 dalem16 35816 dalem17 35817 dalem18 35818 dalem19 35819 dalemswapyzps 35827 dalemcjden 35829 dalem21 35831 dalem22 35832 dalem23 35833 dalem24 35834 dalem25 35835 dalem27 35836 dalem28 35837 dalem38 35847 dalem39 35848 dalem41 35850 dalem42 35851 dalem43 35852 dalem44 35853 dalem45 35854 dalem51 35860 dalem52 35861 dalem54 35863 dalem55 35864 dalem56 35865 dalem57 35866 dalem58 35867 dalem59 35868 dalem60 35869