Colors of
variables: wff setvar class |
Syntax hints: wn 3
wi 4
wo 357
wa 358
wceq 1642
wcel 1710
cab 2339
cif 3663 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675
ax-6 1729 ax-7 1734 ax-11 1746 ax-12 1925 ax-ext 2334 |
This theorem depends on definitions:
df-bi 177 df-or 359
df-an 360 df-tru 1319 df-ex 1542 df-nf 1545 df-sb 1649 df-clab 2340 df-cleq 2346 df-clel 2349 df-if 3664 |
This theorem is referenced by: ifnefalse
3671 ifsb
3672 ifbi
3680 ifeq1da
3688 ifclda
3690 elimif
3692 ifbothda
3693 ifid
3695 ifeqor
3700 ifnot
3701 ifan
3702 ifor
3703 elimhyp
3711 elimhyp2v
3712 elimhyp3v
3713 elimhyp4v
3714 elimdhyp
3716 keephyp2v
3718 keephyp3v
3719 setswith
4322 dfiota3
4371 eqtfinrelk
4487 tfinprop
4490 dfphi2
4570 phi11lem1
4596 0cnelphi
4598 phidisjnn
4616 elimdelov
5574 enprmaplem5
6081 |