![]() |
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 2085 | . 2 ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴) | |
3 | 1, 2 | mpbi 143 | 1 ⊢ 𝐵 = 𝐴 |
Colors of variables: wff set class |
Syntax hints: = wceq 1285 |
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 1377 ax-gen 1379 ax-ext 2065 |
This theorem depends on definitions: df-bi 115 df-cleq 2076 |
This theorem is referenced by: eqtr2i 2104 eqtr3i 2105 eqtr4i 2106 syl5eqr 2129 syl5reqr 2130 syl6eqr 2133 syl6reqr 2134 eqeltrri 2156 eleqtrri 2158 syl5eqelr 2170 syl6eleqr 2176 abid2 2203 abid2f 2247 eqnetrri 2274 neeqtrri 2278 eqsstr3i 3041 sseqtr4i 3043 syl5eqssr 3055 syl6sseqr 3057 difdif2ss 3239 inrab2 3255 dfopg 3594 opid 3614 eqbrtrri 3832 breqtrri 3836 syl6breqr 3851 pwin 4073 limon 4293 tfis 4361 dfdm2 4919 cnvresid 5041 fores 5190 funcoeqres 5232 f1oprg 5243 fmptpr 5431 fsnunres 5440 riotaprop 5570 fo1st 5863 fo2nd 5864 phplem4 6501 snnen2og 6505 phplem4on 6513 eldju 6666 casefun 6683 exmidfodomrlemim 6730 caucvgsrlembound 7242 ax0id 7316 1p1e2 8432 1e2m1 8434 2p1e3 8442 3p1e4 8444 4p1e5 8445 5p1e6 8446 6p1e7 8447 7p1e8 8448 8p1e9 8449 div4p1lem1div2 8561 0mnnnnn0 8597 zeo 8747 num0u 8782 numsucc 8811 decsucc 8812 1e0p1 8813 nummac 8816 decsubi 8834 decmul1 8835 decmul10add 8840 6p5lem 8841 10m1e9 8867 5t5e25 8874 6t6e36 8879 8t6e48 8890 decbin3 8913 infrenegsupex 8977 ige3m2fz 9358 fseq1p1m1 9401 fz0tp 9426 1fv 9440 fzo0to42pr 9520 fzosplitprm1 9534 expnegap0 9800 3dec 9958 fihashen1 10042 pr0hash2ex 10058 imi 10161 3dvdsdec 10645 3dvds2dec 10646 flodddiv4 10714 lcmneg 10836 ex-ceil 10997 ex-gcd 11001 bdceqir 11078 bj-ssom 11174 |
Copyright terms: Public domain | W3C validator |