Step |
Hyp |
Ref |
Expression |
1 |
|
bnj1040.1 |
Could not format ( ph' <-> [. j / i ]. ph ) : No typesetting found for |- ( ph' <-> [. j / i ]. ph ) with typecode |- |
2 |
|
bnj1040.2 |
Could not format ( ps' <-> [. j / i ]. ps ) : No typesetting found for |- ( ps' <-> [. j / i ]. ps ) with typecode |- |
3 |
|
bnj1040.3 |
|
4 |
|
bnj1040.4 |
Could not format ( ch' <-> [. j / i ]. ch ) : No typesetting found for |- ( ch' <-> [. j / i ]. ch ) with typecode |- |
5 |
3
|
sbcbii |
|
6 |
|
df-bnj17 |
|
7 |
|
vex |
|
8 |
7
|
bnj525 |
|
9 |
8
|
bicomi |
|
10 |
7
|
bnj525 |
|
11 |
10
|
bicomi |
|
12 |
9 11 1 2
|
bnj887 |
Could not format ( ( n e. D /\ f Fn n /\ ph' /\ ps' ) <-> ( [. j / i ]. n e. D /\ [. j / i ]. f Fn n /\ [. j / i ]. ph /\ [. j / i ]. ps ) ) : No typesetting found for |- ( ( n e. D /\ f Fn n /\ ph' /\ ps' ) <-> ( [. j / i ]. n e. D /\ [. j / i ]. f Fn n /\ [. j / i ]. ph /\ [. j / i ]. ps ) ) with typecode |- |
13 |
|
df-bnj17 |
|
14 |
13
|
sbcbii |
|
15 |
|
sbcan |
|
16 |
|
sbc3an |
|
17 |
16
|
anbi1i |
|
18 |
14 15 17
|
3bitri |
|
19 |
6 12 18
|
3bitr4ri |
Could not format ( [. j / i ]. ( n e. D /\ f Fn n /\ ph /\ ps ) <-> ( n e. D /\ f Fn n /\ ph' /\ ps' ) ) : No typesetting found for |- ( [. j / i ]. ( n e. D /\ f Fn n /\ ph /\ ps ) <-> ( n e. D /\ f Fn n /\ ph' /\ ps' ) ) with typecode |- |
20 |
4 5 19
|
3bitri |
Could not format ( ch' <-> ( n e. D /\ f Fn n /\ ph' /\ ps' ) ) : No typesetting found for |- ( ch' <-> ( n e. D /\ f Fn n /\ ph' /\ ps' ) ) with typecode |- |