![]() |
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 | ⊢ A = B |
Ref | Expression |
---|---|
eqcomi | ⊢ B = A |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqcomi.1 | . 2 ⊢ A = B | |
2 | eqcom 2039 | . 2 ⊢ (A = B ↔ B = A) | |
3 | 1, 2 | mpbi 133 | 1 ⊢ B = A |
Colors of variables: wff set class |
Syntax hints: = wceq 1242 |
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 1333 ax-gen 1335 ax-ext 2019 |
This theorem depends on definitions: df-bi 110 df-cleq 2030 |
This theorem is referenced by: eqtr2i 2058 eqtr3i 2059 eqtr4i 2060 syl5eqr 2083 syl5reqr 2084 syl6eqr 2087 syl6reqr 2088 eqeltrri 2108 eleqtrri 2110 syl5eqelr 2122 syl6eleqr 2128 abid2 2155 abid2f 2199 eqnetrri 2224 neeqtrri 2228 eqsstr3i 2970 sseqtr4i 2972 syl5eqssr 2984 syl6sseqr 2986 difdif2ss 3188 inrab2 3204 dfopg 3538 opid 3558 eqbrtrri 3776 breqtrri 3780 syl6breqr 3795 pwin 4010 limon 4204 tfis 4249 dfdm2 4795 cnvresid 4916 fores 5058 funcoeqres 5100 f1oprg 5111 fmptpr 5298 fsnunres 5307 riotaprop 5434 fo1st 5726 fo2nd 5727 ax0id 6762 1p1e2 7811 1e2m1 7813 2p1e3 7821 3p1e4 7823 4p1e5 7824 5p1e6 7825 6p1e7 7826 7p1e8 7827 8p1e9 7828 9p1e10 7829 0mnnnnn0 7990 zeo 8119 num0u 8152 numsucc 8169 1e0p1 8171 nummac 8175 6p5lem 8192 5t5e25 8219 6t6e36 8224 8t6e48 8235 decbin3 8248 ige3m2fz 8683 fseq1p1m1 8726 fz0tp 8751 1fv 8766 fzo0to42pr 8846 fzosplitprm1 8860 expnegap0 8917 imi 9128 bdceqir 9299 bj-ssom 9395 |
Copyright terms: Public domain | W3C validator |