![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eqeq1d | GIF version |
Description: Deduction from equality to equivalence of equalities. (Contributed by NM, 27-Dec-1993.) |
Ref | Expression |
---|---|
eqeq1d.1 | ⊢ (φ → A = B) |
Ref | Expression |
---|---|
eqeq1d | ⊢ (φ → (A = 𝐶 ↔ B = 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqeq1d.1 | . 2 ⊢ (φ → A = B) | |
2 | eqeq1 2043 | . 2 ⊢ (A = B → (A = 𝐶 ↔ B = 𝐶)) | |
3 | 1, 2 | syl 14 | 1 ⊢ (φ → (A = 𝐶 ↔ B = 𝐶)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 98 = 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-4 1397 ax-17 1416 ax-ext 2019 |
This theorem depends on definitions: df-bi 110 df-cleq 2030 |
This theorem is referenced by: sbceq2g 2866 csbhypf 2879 csbiebt 2880 csbiebg 2883 disjssun 3279 sneqrg 3524 preq12b 3532 preq12bg 3535 iin0r 3913 opthg 3966 opeqsn 3980 unisucg 4117 opthreg 4234 tfisi 4253 dmsnopg 4735 relcoi1 4792 iotaeq 4818 iotabi 4819 fneq1 4930 fnun 4948 fnresdisj 4952 fnimadisj 4962 fnimaeq0 4963 sbcfng 4987 foeq1 5045 foco 5059 fvelimab 5172 fvun1 5182 fvmptdv2 5203 fneqeql 5218 dffo3 5257 fvsng 5302 fconstfvm 5322 eufnfv 5332 f1veqaeq 5351 dff13f 5352 f1elima 5355 foeqcnvco 5373 f1eqcocnv 5374 acexmidlemab 5449 eloprabga 5533 ovmpt2dv2 5576 ovi3 5579 ovelimab 5593 caovcang 5604 caovcan 5607 caovimo 5636 grprinvlem 5637 grpridd 5639 suppssfv 5650 suppssov1 5651 caofinvl 5675 op1stg 5719 op2ndg 5720 eqop 5745 reldm 5754 xporderlem 5793 tposfo2 5823 frec0g 5922 frecsuclem3 5929 frecsuc 5930 nnm0r 5997 nnmord 6026 nnaordex 6036 nnawordex 6037 ereq1 6049 eqerlem 6073 endisj 6234 addnidpig 6320 ltexpi 6321 dfplpq2 6338 dfmpq2 6339 recexnq 6374 recmulnqg 6375 ltexnqq 6391 halfnqq 6393 enq0tr 6417 nqnq0pi 6421 addnnnq0 6432 addlocpr 6519 ltexprlemru 6586 ltexpri 6587 recexpr 6610 addsrpr 6673 mulsrpr 6674 00sr 6697 negexsr 6700 recexgt0sr 6701 axrnegex 6763 axprecex 6764 cnegexlem1 6983 cnegex 6986 cnegex2 6987 subval 7000 subadd 7011 subadd2 7012 subsub23 7013 addsubeq4 7023 subcan2 7032 negcon1 7059 subcan 7062 ltadd2 7212 recexre 7362 recexap 7416 muleqadd 7431 receuap 7432 divvalap 7435 divmulap 7436 rec11ap 7468 zdiv 8104 uzin 8281 icc0r 8565 fznlem 8675 fseq1m1p1 8727 1fv 8766 fzon 8792 frecuzrdgfn 8879 mulreap 9092 rennim 9211 |
Copyright terms: Public domain | W3C validator |