![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eqcomi | GIF version |
Description: Inference from commutative law for class equality. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
eqcomi.1 | ⊢ 𝐴 = 𝐵 |
Ref | Expression |
---|---|
eqcomi | ⊢ 𝐵 = 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqcomi.1 | . 2 ⊢ 𝐴 = 𝐵 | |
2 | eqcom 2117 | . 2 ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴) | |
3 | 1, 2 | mpbi 144 | 1 ⊢ 𝐵 = 𝐴 |
Colors of variables: wff set class |
Syntax hints: = wceq 1314 |
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-ext 2097 |
This theorem depends on definitions: df-bi 116 df-cleq 2108 |
This theorem is referenced by: eqtr2i 2136 eqtr3i 2137 eqtr4i 2138 syl5eqr 2161 syl5reqr 2162 syl6eqr 2165 syl6reqr 2166 eqeltrri 2188 eleqtrri 2190 syl5eqelr 2202 syl6eleqr 2208 abid2 2235 abid2f 2280 eqnetrri 2307 neeqtrri 2311 eqsstrri 3096 sseqtr4i 3098 eqsstrrid 3110 syl6sseqr 3112 difdif2ss 3299 inrab2 3315 dfopg 3669 opid 3689 eqbrtrri 3916 breqtrri 3920 syl6breqr 3935 pwin 4164 limon 4389 tfis 4457 dfdm2 5031 cnvresid 5155 fores 5312 funcoeqres 5354 f1oprg 5365 fmptpr 5566 fsnunres 5576 riotaprop 5707 fo1st 6009 fo2nd 6010 fnmpoovd 6066 ixpsnf1o 6584 phplem4 6702 snnen2og 6706 phplem4on 6714 sbthlemi5 6801 eldju 6905 casefun 6922 omp1eomlem 6931 exmidfodomrlemim 7005 caucvgsrlembound 7536 ax0id 7613 1p1e2 8747 1e2m1 8749 2p1e3 8757 3p1e4 8759 4p1e5 8760 5p1e6 8761 6p1e7 8762 7p1e8 8763 8p1e9 8764 div4p1lem1div2 8877 0mnnnnn0 8913 zeo 9060 num0u 9096 numsucc 9125 decsucc 9126 1e0p1 9127 nummac 9130 decsubi 9148 decmul1 9149 decmul10add 9154 6p5lem 9155 10m1e9 9181 5t5e25 9188 6t6e36 9193 8t6e48 9204 decbin3 9227 infrenegsupex 9291 ige3m2fz 9722 fseq1p1m1 9767 fz0tp 9794 1fv 9809 fzo0to42pr 9890 fzosplitprm1 9904 expnegap0 10194 sq4e2t8 10283 3dec 10354 fihashen1 10438 pr0hash2ex 10454 imi 10565 infxrnegsupex 10924 zsumdc 11045 fsumadd 11067 hashrabrex 11142 efsep 11248 3dvdsdec 11410 3dvds2dec 11411 flodddiv4 11479 lcmneg 11601 ennnfonelem1 11765 ndxid 11826 2strstr1g 11905 toponrestid 12031 istpsi 12049 distopon 12099 distps 12103 discld 12148 txbas 12269 txdis 12288 txdis1cn 12289 ex-ceil 12631 ex-gcd 12636 bdceqir 12734 bj-ssom 12826 trilpolemgt1 12924 |
Copyright terms: Public domain | W3C validator |