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 2119 | . 2 ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴) | |
3 | 1, 2 | mpbi 144 | 1 ⊢ 𝐵 = 𝐴 |
Colors of variables: wff set class |
Syntax hints: = wceq 1316 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1408 ax-gen 1410 ax-ext 2099 |
This theorem depends on definitions: df-bi 116 df-cleq 2110 |
This theorem is referenced by: eqtr2i 2139 eqtr3i 2140 eqtr4i 2141 syl5eqr 2164 syl5reqr 2165 syl6eqr 2168 syl6reqr 2169 eqeltrri 2191 eleqtrri 2193 eqeltrrid 2205 eleqtrrdi 2211 abid2 2238 abid2f 2283 eqnetrri 2310 neeqtrri 2314 eqsstrri 3100 sseqtrri 3102 eqsstrrid 3114 sseqtrrdi 3116 difdif2ss 3303 inrab2 3319 dfopg 3673 opid 3693 eqbrtrri 3921 breqtrri 3925 breqtrrdi 3940 pwin 4174 limon 4399 tfis 4467 dfdm2 5043 cnvresid 5167 fores 5324 funcoeqres 5366 f1oprg 5379 fmptpr 5580 fsnunres 5590 riotaprop 5721 fo1st 6023 fo2nd 6024 fnmpoovd 6080 ixpsnf1o 6598 phplem4 6717 snnen2og 6721 phplem4on 6729 sbthlemi5 6817 eldju 6921 casefun 6938 omp1eomlem 6947 exmidfodomrlemim 7025 caucvgsrlembound 7570 ax0id 7654 1p1e2 8801 1e2m1 8803 2p1e3 8811 3p1e4 8813 4p1e5 8814 5p1e6 8815 6p1e7 8816 7p1e8 8817 8p1e9 8818 div4p1lem1div2 8931 0mnnnnn0 8967 zeo 9114 num0u 9150 numsucc 9179 decsucc 9180 1e0p1 9181 nummac 9184 decsubi 9202 decmul1 9203 decmul10add 9208 6p5lem 9209 10m1e9 9235 5t5e25 9242 6t6e36 9247 8t6e48 9258 decbin3 9281 infrenegsupex 9345 ige3m2fz 9784 fseq1p1m1 9829 fz0tp 9856 1fv 9871 fzo0to42pr 9952 fzosplitprm1 9966 expnegap0 10256 sq4e2t8 10345 3dec 10416 fihashen1 10500 pr0hash2ex 10516 imi 10627 infxrnegsupex 10987 zsumdc 11108 fsumadd 11130 hashrabrex 11205 efsep 11311 3dvdsdec 11474 3dvds2dec 11475 flodddiv4 11543 lcmneg 11667 ennnfonelem1 11831 ndxid 11894 2strstr1g 11973 toponrestid 12099 istpsi 12117 distopon 12167 distps 12171 discld 12216 txbas 12338 txdis 12357 txdis1cn 12358 txhmeo 12399 txswaphmeolem 12400 dvexp 12755 sinq34lt0t 12823 ex-ceil 12834 ex-gcd 12839 bdceqir 12938 bj-ssom 13030 trilpolemgt1 13128 |
Copyright terms: Public domain | W3C validator |