![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eqeq1i | Unicode version |
Description: Inference from equality to equivalence of equalities. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
eqeq1i.1 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
eqeq1i |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqeq1i.1 |
. 2
![]() ![]() ![]() ![]() | |
2 | eqeq1 2094 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ax-mp 7 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-5 1381 ax-gen 1383 ax-4 1445 ax-17 1464 ax-ext 2070 |
This theorem depends on definitions: df-bi 115 df-cleq 2081 |
This theorem is referenced by: ssequn2 3173 dfss1 3204 disj 3331 disjr 3332 undisj1 3340 undisj2 3341 uneqdifeqim 3368 reusn 3513 rabsneu 3515 eusn 3516 iin0r 4004 opeqsn 4079 unisuc 4240 onsucelsucexmid 4346 sucprcreg 4365 onintexmid 4388 dmopab3 4649 dm0rn0 4653 ssdmres 4735 imadisj 4794 args 4801 intirr 4818 dminxp 4875 dfrel3 4888 fntpg 5070 fncnv 5080 f0rn0 5205 dff1o4 5261 dffv4g 5302 fvun2 5371 fnreseql 5409 riota1 5626 riota2df 5628 fnotovb 5692 ovid 5761 ov 5764 ovg 5783 f1od2 6000 frec0g 6162 diffitest 6603 prarloclem5 7059 renegcl 7743 elznn0 8765 hashunlem 10212 maxclpr 10655 ex-ceil 11653 nninfsellemqall 11907 nninfomni 11911 |
Copyright terms: Public domain | W3C validator |