dftap2 - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > dftap2		Unicode version

Theorem dftap2 7318

Description: Tight apartness with the apartness properties from df-pap 7315 expanded. (Contributed by Jim Kingdon, 21-Feb-2025.)

**Assertion**
Ref	Expression
dftap2	TAp $/\$ $/\$ $/\$ $\/$ $/\$

**Proof of Theorem dftap2**
Step	Hyp	Ref	Expression
1		df-tap 7317	. . . . . . . 8 TAp Ap $/\$
2	1	biimpi 120	. . . . . . 7 TAp Ap $/\$
3	2	simpld 112	. . . . . 6 TAp Ap
4		df-pap 7315	. . . . . 6 Ap $/\$ $/\$ $/\$ $\/$
5	3, 4	sylib 122	. . . . 5 TAp $/\$ $/\$ $/\$ $\/$
6	5	simpld 112	. . . 4 TAp $/\$
7	6	simpld 112	. . 3 TAp
8	6	simprd 114	. . . 4 TAp
9	5	simprd 114	. . . . 5 TAp $/\$ $\/$
10	9	simpld 112	. . . 4 TAp
11	8, 10	jca 306	. . 3 TAp $/\$
12	9	simprd 114	. . . 4 TAp $\/$
13	2	simprd 114	. . . 4 TAp
14	12, 13	jca 306	. . 3 TAp $\/$ $/\$
15	7, 11, 14	3jca 1179	. 2 TAp $/\$ $/\$ $/\$ $\/$ $/\$
16		simp1 999	. . . . 5 $/\$ $/\$ $/\$ $\/$ $/\$
17		simp2l 1025	. . . . 5 $/\$ $/\$ $/\$ $\/$ $/\$
18	16, 17	jca 306	. . . 4 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
19		simp2r 1026	. . . . 5 $/\$ $/\$ $/\$ $\/$ $/\$
20		simp3l 1027	. . . . 5 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$
21	19, 20	jca 306	. . . 4 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$
22	18, 21, 4	sylanbrc 417	. . 3 $/\$ $/\$ $/\$ $\/$ $/\$ Ap
23		simp3r 1028	. . 3 $/\$ $/\$ $/\$ $\/$ $/\$
24	22, 23, 1	sylanbrc 417	. 2 $/\$ $/\$ $/\$ $\/$ $/\$ TAp
25	15, 24	impbii 126	1 TAp $/\$ $/\$ $/\$ $\/$ $/\$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 104

wb 105 $\/$ wo 709 $/\$ w3a 980

wral 2475

wss 3157 class class class wbr 4033

cxp 4661 Ap wap 7314 TAp wtap 7316

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108

This theorem depends on definitions: df-bi 117 df-3an 982 df-pap 7315 df-tap 7317

This theorem is referenced by: tapeq1 7319 tapeq2 7320 netap 7321 2omotaplemap 7324 exmidapne 7327 aptap 8677