![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eqcomd | GIF version |
Description: Deduction from commutative law for class equality. (Contributed by NM, 15-Aug-1994.) |
Ref | Expression |
---|---|
eqcomd.1 | ⊢ (φ → A = B) |
Ref | Expression |
---|---|
eqcomd | ⊢ (φ → B = A) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqcomd.1 | . 2 ⊢ (φ → A = B) | |
2 | eqcom 2039 | . 2 ⊢ (A = B ↔ B = A) | |
3 | 1, 2 | sylib 127 | 1 ⊢ (φ → B = A) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = 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: eqtr2d 2070 eqtr3d 2071 eqtr4d 2072 syl5req 2082 syl6req 2086 sylan9req 2090 eqeltrrd 2112 eleqtrrd 2114 syl5eleqr 2124 syl6eqelr 2126 eqnetrrd 2225 neeqtrrd 2229 dedhb 2704 eqsstr3d 2974 sseqtr4d 2976 syl6eqssr 2990 dfrab3ss 3209 uneqdifeqim 3302 disjsn2 3424 diftpsn3 3496 dfopg 3538 unimax 3605 sndisj 3751 eqbrtrrd 3777 breqtrrd 3781 syl5breqr 3791 syl6eqbrr 3793 class2seteq 3907 opth1 3964 euotd 3982 opelopabsb 3988 tfisi 4253 0nelxp 4315 opeliunxp 4338 euiotaex 4826 iota4 4828 fun2ssres 4886 funimass1 4919 funssfv 5142 fnimapr 5176 fvun1 5182 fmptco 5273 foeqcnvco 5373 f1eqcocnv 5374 f1oiso2 5409 riotass2 5437 riotass 5438 f1ocnvfv3 5444 caovlem2d 5635 f1opw2 5648 sbcopeq1a 5755 csbopeq1a 5756 eloprabi 5764 cnvf1olem 5787 f2ndf 5789 smoiso 5858 nnaword 6020 eqer 6074 uniqs 6100 enq0sym 6415 enq0tr 6417 recexgt0sr 6701 le2tri3i 6923 cnegexlem2 6984 nnpcan 7030 subdi 7178 rereim 7370 cru 7386 divap1d 7558 elz2 8088 zindd 8132 qapne 8350 xrlttri3 8488 fseq1p1m1 8726 fzrevral 8737 nn0disj 8765 fzosplitsnm1 8835 fzosplitprm1 8860 frecuzrdgsuc 8882 frecfzen2 8885 expgt1 8947 leexp2r 8962 replim 9087 cjexp 9121 |
Copyright terms: Public domain | W3C validator |