Step |
Hyp |
Ref |
Expression |
1 |
|
bnj130.1 |
|
2 |
|
bnj130.2 |
Could not format ( ph' <-> [. 1o / n ]. ph ) : No typesetting found for |- ( ph' <-> [. 1o / n ]. ph ) with typecode |- |
3 |
|
bnj130.3 |
Could not format ( ps' <-> [. 1o / n ]. ps ) : No typesetting found for |- ( ps' <-> [. 1o / n ]. ps ) with typecode |- |
4 |
|
bnj130.4 |
Could not format ( th' <-> [. 1o / n ]. th ) : No typesetting found for |- ( th' <-> [. 1o / n ]. th ) with typecode |- |
5 |
1
|
sbcbii |
|
6 |
|
bnj105 |
|
7 |
6
|
bnj90 |
|
8 |
7
|
bicomi |
|
9 |
8 2 3
|
3anbi123i |
Could not format ( ( f Fn 1o /\ ph' /\ ps' ) <-> ( [. 1o / n ]. f Fn n /\ [. 1o / n ]. ph /\ [. 1o / n ]. ps ) ) : No typesetting found for |- ( ( f Fn 1o /\ ph' /\ ps' ) <-> ( [. 1o / n ]. f Fn n /\ [. 1o / n ]. ph /\ [. 1o / n ]. ps ) ) with typecode |- |
10 |
|
sbc3an |
|
11 |
9 10
|
bitr4i |
Could not format ( ( f Fn 1o /\ ph' /\ ps' ) <-> [. 1o / n ]. ( f Fn n /\ ph /\ ps ) ) : No typesetting found for |- ( ( f Fn 1o /\ ph' /\ ps' ) <-> [. 1o / n ]. ( f Fn n /\ ph /\ ps ) ) with typecode |- |
12 |
11
|
eubii |
Could not format ( E! f ( f Fn 1o /\ ph' /\ ps' ) <-> E! f [. 1o / n ]. ( f Fn n /\ ph /\ ps ) ) : No typesetting found for |- ( E! f ( f Fn 1o /\ ph' /\ ps' ) <-> E! f [. 1o / n ]. ( f Fn n /\ ph /\ ps ) ) with typecode |- |
13 |
6
|
bnj89 |
|
14 |
12 13
|
bitr4i |
Could not format ( E! f ( f Fn 1o /\ ph' /\ ps' ) <-> [. 1o / n ]. E! f ( f Fn n /\ ph /\ ps ) ) : No typesetting found for |- ( E! f ( f Fn 1o /\ ph' /\ ps' ) <-> [. 1o / n ]. E! f ( f Fn n /\ ph /\ ps ) ) with typecode |- |
15 |
14
|
imbi2i |
Could not format ( ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn 1o /\ ph' /\ ps' ) ) <-> ( ( R _FrSe A /\ x e. A ) -> [. 1o / n ]. E! f ( f Fn n /\ ph /\ ps ) ) ) : No typesetting found for |- ( ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn 1o /\ ph' /\ ps' ) ) <-> ( ( R _FrSe A /\ x e. A ) -> [. 1o / n ]. E! f ( f Fn n /\ ph /\ ps ) ) ) with typecode |- |
16 |
|
nfv |
|
17 |
16
|
sbc19.21g |
|
18 |
6 17
|
ax-mp |
|
19 |
15 18
|
bitr4i |
Could not format ( ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn 1o /\ ph' /\ ps' ) ) <-> [. 1o / n ]. ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn n /\ ph /\ ps ) ) ) : No typesetting found for |- ( ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn 1o /\ ph' /\ ps' ) ) <-> [. 1o / n ]. ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn n /\ ph /\ ps ) ) ) with typecode |- |
20 |
5 4 19
|
3bitr4i |
Could not format ( th' <-> ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn 1o /\ ph' /\ ps' ) ) ) : No typesetting found for |- ( th' <-> ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn 1o /\ ph' /\ ps' ) ) ) with typecode |- |