Step |
Hyp |
Ref |
Expression |
1 |
|
bnj910.1 |
|
2 |
|
bnj910.2 |
|
3 |
|
bnj910.3 |
|
4 |
|
bnj910.4 |
Could not format ( ph' <-> [. p / n ]. ph ) : No typesetting found for |- ( ph' <-> [. p / n ]. ph ) with typecode |- |
5 |
|
bnj910.5 |
Could not format ( ps' <-> [. p / n ]. ps ) : No typesetting found for |- ( ps' <-> [. p / n ]. ps ) with typecode |- |
6 |
|
bnj910.6 |
Could not format ( ch' <-> [. p / n ]. ch ) : No typesetting found for |- ( ch' <-> [. p / n ]. ch ) with typecode |- |
7 |
|
bnj910.7 |
Could not format ( ph" <-> [. G / f ]. ph' ) : No typesetting found for |- ( ph" <-> [. G / f ]. ph' ) with typecode |- |
8 |
|
bnj910.8 |
Could not format ( ps" <-> [. G / f ]. ps' ) : No typesetting found for |- ( ps" <-> [. G / f ]. ps' ) with typecode |- |
9 |
|
bnj910.9 |
Could not format ( ch" <-> [. G / f ]. ch' ) : No typesetting found for |- ( ch" <-> [. G / f ]. ch' ) with typecode |- |
10 |
|
bnj910.10 |
|
11 |
|
bnj910.11 |
|
12 |
|
bnj910.12 |
|
13 |
|
bnj910.13 |
|
14 |
|
bnj910.14 |
|
15 |
|
bnj910.15 |
|
16 |
3 10
|
bnj970 |
|
17 |
1 2 3 10 12 14 15
|
bnj969 |
|
18 |
|
simpr3 |
|
19 |
3
|
bnj1235 |
|
20 |
19
|
3ad2ant1 |
|
21 |
20
|
adantl |
|
22 |
13
|
bnj941 |
|
23 |
22
|
3impib |
|
24 |
17 18 21 23
|
syl3anc |
|
25 |
1 2 3 4 7 10 12 13 14 15
|
bnj944 |
Could not format ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> ph" ) : No typesetting found for |- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> ph" ) with typecode |- |
26 |
2 3 10 12 13 17
|
bnj967 |
|
27 |
3 10 12 13 17 24
|
bnj966 |
|
28 |
2 3 5 8 12 13 26 27
|
bnj964 |
Could not format ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> ps" ) : No typesetting found for |- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> ps" ) with typecode |- |
29 |
16 24 25 28
|
bnj951 |
Could not format ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> ( p e. D /\ G Fn p /\ ph" /\ ps" ) ) : No typesetting found for |- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> ( p e. D /\ G Fn p /\ ph" /\ ps" ) ) with typecode |- |
30 |
|
vex |
|
31 |
3 4 5 6 30
|
bnj919 |
Could not format ( ch' <-> ( p e. D /\ f Fn p /\ ph' /\ ps' ) ) : No typesetting found for |- ( ch' <-> ( p e. D /\ f Fn p /\ ph' /\ ps' ) ) with typecode |- |
32 |
13
|
bnj918 |
|
33 |
31 7 8 9 32
|
bnj976 |
Could not format ( ch" <-> ( p e. D /\ G Fn p /\ ph" /\ ps" ) ) : No typesetting found for |- ( ch" <-> ( p e. D /\ G Fn p /\ ph" /\ ps" ) ) with typecode |- |
34 |
29 33
|
sylibr |
Could not format ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> ch" ) : No typesetting found for |- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> ch" ) with typecode |- |