![]() |
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 2042 | . 2 ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴) | |
3 | 1, 2 | mpbi 133 | 1 ⊢ 𝐵 = 𝐴 |
Colors of variables: wff set class |
Syntax hints: = wceq 1243 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1336 ax-gen 1338 ax-ext 2022 |
This theorem depends on definitions: df-bi 110 df-cleq 2033 |
This theorem is referenced by: eqtr2i 2061 eqtr3i 2062 eqtr4i 2063 syl5eqr 2086 syl5reqr 2087 syl6eqr 2090 syl6reqr 2091 eqeltrri 2111 eleqtrri 2113 syl5eqelr 2125 syl6eleqr 2131 abid2 2158 abid2f 2202 eqnetrri 2230 neeqtrri 2234 eqsstr3i 2976 sseqtr4i 2978 syl5eqssr 2990 syl6sseqr 2992 difdif2ss 3194 inrab2 3210 dfopg 3547 opid 3567 eqbrtrri 3785 breqtrri 3789 syl6breqr 3804 pwin 4019 limon 4239 tfis 4306 dfdm2 4852 cnvresid 4973 fores 5115 funcoeqres 5157 f1oprg 5168 fmptpr 5355 fsnunres 5364 riotaprop 5491 fo1st 5784 fo2nd 5785 phplem4 6318 snnen2og 6322 phplem4on 6329 caucvgsrlembound 6878 ax0id 6952 1p1e2 8033 1e2m1 8035 2p1e3 8043 3p1e4 8045 4p1e5 8046 5p1e6 8047 6p1e7 8048 7p1e8 8049 8p1e9 8050 9p1e10 8051 div4p1lem1div2 8177 0mnnnnn0 8214 zeo 8343 num0u 8376 numsucc 8393 1e0p1 8395 nummac 8399 6p5lem 8416 5t5e25 8443 6t6e36 8448 8t6e48 8459 decbin3 8472 ige3m2fz 8913 fseq1p1m1 8956 fz0tp 8981 1fv 8996 fzo0to42pr 9076 fzosplitprm1 9090 expnegap0 9263 imi 9500 ex-ceil 9896 bdceqir 9964 bj-ssom 10060 |
Copyright terms: Public domain | W3C validator |