![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > equequ2 | Unicode version |
Description: An equivalence law for equality. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
equequ2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | equtrr 1710 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | equtrr 1710 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | equcoms 1708 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | impbid 129 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-gen 1449 ax-ie2 1494 ax-8 1504 ax-17 1526 ax-i9 1530 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: ax11v2 1820 ax11v 1827 ax11ev 1828 equs5or 1830 eujust 2028 euf 2031 mo23 2067 eleq1w 2238 cbvabw 2300 csbcow 3068 disjiun 3998 iotaval 5189 dffun4f 5232 dff13f 5770 supmoti 6991 isoti 7005 nninfwlpoim 7175 exmidontriim 7223 netap 7252 ennnfonelemr 12418 ctinf 12425 infpn2 12451 |
Copyright terms: Public domain | W3C validator |