wl-exeq - Mathbox for Wolf Lammen

	Mathbox for Wolf Lammen		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > wl-exeq		Structured version Visualization version Unicode version

Theorem wl-exeq 33321

Description: The semantics of

. (Contributed by Wolf Lammen, 27-Apr-2018.)

**Assertion**
Ref	Expression
wl-exeq	$\/$ $\/$

**Proof of Theorem wl-exeq**
Step	Hyp	Ref	Expression
1		nfeqf 2301	. . . . . . . 8 $/\$
2	1	19.9d 2070	. . . . . . 7 $/\$
3	2	impancom 456	. . . . . 6 $/\$
4	3	orrd 393	. . . . 5 $/\$ $\/$
5	4	expcom 451	. . . 4 $\/$
6	5	orrd 393	. . 3 $\/$ $\/$
7		3orrot 1044	. . . 4 $\/$ $\/$ $\/$ $\/$
8		3orass 1040	. . . 4 $\/$ $\/$ $\/$ $\/$
9	7, 8	bitri 264	. . 3 $\/$ $\/$ $\/$ $\/$
10	6, 9	sylibr 224	. 2 $\/$ $\/$
11		19.8a 2052	. . 3
12		ax6e 2250	. . . . 5
13		ax7 1943	. . . . . 6
14	13	com12 32	. . . . 5
15	12, 14	eximii 1764	. . . 4
16	15	19.35i 1806	. . 3
17		ax6e 2250	. . . . 5
18	17, 13	eximii 1764	. . . 4
19	18	19.35i 1806	. . 3
20	11, 16, 19	3jaoi 1391	. 2 $\/$ $\/$
21	10, 20	impbii 199	1 $\/$ $\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 196 $\/$ wo 383 $/\$ wa 384 $\/$ w3o 1036

wal 1481

wex 1704

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-10 2019 ax-12 2047 ax-13 2246

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710

This theorem is referenced by: wl-nfeqfb 33323