![]() |
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 2121 |
. 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 105 ax-ia2 106 ax-ia3 107 ax-5 1406 ax-gen 1408 ax-4 1470 ax-17 1489 ax-ext 2097 |
This theorem depends on definitions: df-bi 116 df-cleq 2108 |
This theorem is referenced by: ssequn2 3215 dfss1 3246 disj 3377 disjr 3378 undisj1 3386 undisj2 3387 uneqdifeqim 3414 reusn 3560 rabsneu 3562 eusn 3563 iin0r 4053 opeqsn 4134 unisuc 4295 onsucelsucexmid 4405 sucprcreg 4424 onintexmid 4447 dmopab3 4712 dm0rn0 4716 ssdmres 4799 imadisj 4859 args 4866 intirr 4883 dminxp 4941 dfrel3 4954 fntpg 5137 fncnv 5147 f0rn0 5275 dff1o4 5331 dffv4g 5372 fvun2 5442 fnreseql 5484 riota1 5702 riota2df 5704 fnotovb 5768 ovid 5841 ov 5844 ovg 5863 f1od2 6086 frec0g 6248 diffitest 6734 ismkvnex 6979 prarloclem5 7256 renegcl 7946 elznn0 8973 hashunlem 10443 maxclpr 10886 ex-ceil 12631 nninfsellemqall 12903 nninfomni 12907 |
Copyright terms: Public domain | W3C validator |