![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eqcomi | Unicode 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 2102 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | mpbi 144 |
1
![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() |
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 1391 ax-gen 1393 ax-ext 2082 |
This theorem depends on definitions: df-bi 116 df-cleq 2093 |
This theorem is referenced by: eqtr2i 2121 eqtr3i 2122 eqtr4i 2123 syl5eqr 2146 syl5reqr 2147 syl6eqr 2150 syl6reqr 2151 eqeltrri 2173 eleqtrri 2175 syl5eqelr 2187 syl6eleqr 2193 abid2 2220 abid2f 2265 eqnetrri 2292 neeqtrri 2296 eqsstr3i 3080 sseqtr4i 3082 syl5eqssr 3094 syl6sseqr 3096 difdif2ss 3280 inrab2 3296 dfopg 3650 opid 3670 eqbrtrri 3896 breqtrri 3900 syl6breqr 3915 pwin 4142 limon 4367 tfis 4435 dfdm2 5009 cnvresid 5133 fores 5290 funcoeqres 5332 f1oprg 5343 fmptpr 5544 fsnunres 5554 riotaprop 5685 fo1st 5986 fo2nd 5987 fnmpoovd 6042 ixpsnf1o 6560 phplem4 6678 snnen2og 6682 phplem4on 6690 sbthlemi5 6777 eldju 6868 casefun 6885 omp1eomlem 6894 exmidfodomrlemim 6966 caucvgsrlembound 7489 ax0id 7563 1p1e2 8695 1e2m1 8697 2p1e3 8705 3p1e4 8707 4p1e5 8708 5p1e6 8709 6p1e7 8710 7p1e8 8711 8p1e9 8712 div4p1lem1div2 8825 0mnnnnn0 8861 zeo 9008 num0u 9044 numsucc 9073 decsucc 9074 1e0p1 9075 nummac 9078 decsubi 9096 decmul1 9097 decmul10add 9102 6p5lem 9103 10m1e9 9129 5t5e25 9136 6t6e36 9141 8t6e48 9152 decbin3 9175 infrenegsupex 9239 ige3m2fz 9670 fseq1p1m1 9715 fz0tp 9742 1fv 9757 fzo0to42pr 9838 fzosplitprm1 9852 expnegap0 10142 sq4e2t8 10231 3dec 10302 fihashen1 10386 pr0hash2ex 10402 imi 10513 infxrnegsupex 10871 zsumdc 10992 fsumadd 11014 hashrabrex 11089 efsep 11195 3dvdsdec 11357 3dvds2dec 11358 flodddiv4 11426 lcmneg 11548 ennnfonelem1 11712 ndxid 11765 2strstr1g 11844 toponrestid 11970 istpsi 11988 distopon 12038 distps 12042 discld 12087 txbas 12208 txdis 12227 txdis1cn 12228 ex-ceil 12541 ex-gcd 12546 bdceqir 12623 bj-ssom 12719 trilpolemgt1 12816 |
Copyright terms: Public domain | W3C validator |