dalemqea - Mathbox for Norm Megill

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

Theorem dalemqea 34913

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

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

**Assertion**
Ref	Expression
dalemqea

**Proof of Theorem dalemqea**
Step	Hyp	Ref	Expression
1		dalema.ph	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
2		simp122 1194	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
3	1, 2	sylbi 207	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 196 $/\$ wa 384 $/\$ w3a 1037

wcel 1990 class class class wbr 4653

cfv 5888 (class class class)co 6650

cbs 15857

chlt 34637

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 197 df-an 386 df-3an 1039

This theorem is referenced by: dalemqeb 34926 dalempjqeb 34931 dalemqrprot 34934 dalemply 34940 dalemswapyz 34942 dalemrot 34943 dalem1 34945 dalemcea 34946 dalem2 34947 dalemdea 34948 dalem3 34950 dalem4 34951 dalem-cly 34957 dalem18 34967 dalem51 35009 dalem52 35010 dalem56 35014