![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > equequ1 | Unicode version |
Description: An equivalence law for equality. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
equequ1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-8 1515 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | equtr 1720 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | 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 1460 ax-ie2 1505 ax-8 1515 ax-17 1537 ax-i9 1541 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: equveli 1770 drsb1 1810 equsb3lem 1962 euequ1 2133 axext3 2172 cbvreuvw 2724 reu6 2941 reu7 2947 disjiun 4016 cbviota 5204 dff13f 5795 poxp 6261 dcdifsnid 6533 supmoti 7026 isoti 7040 nninfwlpoim 7211 exmidontriimlem3 7257 exmidontriim 7259 netap 7288 fsum2dlemstep 11483 ennnfonelemr 12485 ctinf 12492 reap0 15294 |
Copyright terms: Public domain | W3C validator |