Step |
Hyp |
Ref |
Expression |
1 |
|
bnj1097.1 |
|
2 |
|
bnj1097.3 |
|
3 |
|
bnj1097.5 |
|
4 |
1
|
biimpi |
|
5 |
2 4
|
bnj771 |
|
6 |
5
|
3ad2ant3 |
|
7 |
6
|
adantr |
Could not format ( ( ( th /\ ta /\ ch ) /\ ph0 ) -> ( f ` (/) ) = _pred ( X , A , R ) ) : No typesetting found for |- ( ( ( th /\ ta /\ ch ) /\ ph0 ) -> ( f ` (/) ) = _pred ( X , A , R ) ) with typecode |- |
8 |
3
|
simp3bi |
|
9 |
8
|
3ad2ant2 |
|
10 |
9
|
adantr |
Could not format ( ( ( th /\ ta /\ ch ) /\ ph0 ) -> _pred ( X , A , R ) C_ B ) : No typesetting found for |- ( ( ( th /\ ta /\ ch ) /\ ph0 ) -> _pred ( X , A , R ) C_ B ) with typecode |- |
11 |
7 10
|
jca |
Could not format ( ( ( th /\ ta /\ ch ) /\ ph0 ) -> ( ( f ` (/) ) = _pred ( X , A , R ) /\ _pred ( X , A , R ) C_ B ) ) : No typesetting found for |- ( ( ( th /\ ta /\ ch ) /\ ph0 ) -> ( ( f ` (/) ) = _pred ( X , A , R ) /\ _pred ( X , A , R ) C_ B ) ) with typecode |- |
12 |
11
|
anim2i |
Could not format ( ( i = (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( i = (/) /\ ( ( f ` (/) ) = _pred ( X , A , R ) /\ _pred ( X , A , R ) C_ B ) ) ) : No typesetting found for |- ( ( i = (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( i = (/) /\ ( ( f ` (/) ) = _pred ( X , A , R ) /\ _pred ( X , A , R ) C_ B ) ) ) with typecode |- |
13 |
|
3anass |
|
14 |
12 13
|
sylibr |
Could not format ( ( i = (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( i = (/) /\ ( f ` (/) ) = _pred ( X , A , R ) /\ _pred ( X , A , R ) C_ B ) ) : No typesetting found for |- ( ( i = (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( i = (/) /\ ( f ` (/) ) = _pred ( X , A , R ) /\ _pred ( X , A , R ) C_ B ) ) with typecode |- |
15 |
|
fveqeq2 |
|
16 |
15
|
biimpar |
|
17 |
16
|
adantr |
|
18 |
|
simpr |
|
19 |
17 18
|
eqsstrd |
|
20 |
19
|
3impa |
|
21 |
14 20
|
syl |
Could not format ( ( i = (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( f ` i ) C_ B ) : No typesetting found for |- ( ( i = (/) /\ ( ( th /\ ta /\ ch ) /\ ph0 ) ) -> ( f ` i ) C_ B ) with typecode |- |