Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∨ w3o 1087
∀wral 3065 class class class wbr 5106
Po wpo 5544 Or wor 5545 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 |
This theorem depends on definitions:
df-bi 206 df-an 398
df-so 5547 |
This theorem is referenced by: sonr
5569 sotr
5570 so2nr
5572 so3nr
5573 soltmin
6091 predso
6279 tz6.26
6302 wfi
6305 wfisg
6308 wfis2fg
6311 soxp
8062 soseq
8092 wfrfun
8279 wfrresex
8280 wfr2a
8281 wfr1
8282 on2recsfn
8614 on2recsov
8615 on2ind
8616 on3ind
8617 fimax2g
9234 wofi
9237 fimin2g
9434 ordtypelem8
9462 wemaplem2
9484 wemapsolem
9487 cantnf
9630 fin23lem27
10265 iccpnfhmeo
24311 xrhmeo
24312 logccv
26021 ex-po
29382 xrge0iifiso
32519 incsequz2
36211 epirron
41591 oneptr
41592 prproropf1olem1
45702 |