![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > oveq2i | GIF version |
Description: Equality inference for operation value. (Contributed by NM, 28-Feb-1995.) |
Ref | Expression |
---|---|
oveq1i.1 | ⊢ 𝐴 = 𝐵 |
Ref | Expression |
---|---|
oveq2i | ⊢ (𝐶𝐹𝐴) = (𝐶𝐹𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | oveq1i.1 | . 2 ⊢ 𝐴 = 𝐵 | |
2 | oveq2 5734 | . 2 ⊢ (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵)) | |
3 | 1, 2 | ax-mp 7 | 1 ⊢ (𝐶𝐹𝐴) = (𝐶𝐹𝐵) |
Colors of variables: wff set class |
Syntax hints: = wceq 1312 (class class class)co 5726 |
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-io 681 ax-5 1404 ax-7 1405 ax-gen 1406 ax-ie1 1450 ax-ie2 1451 ax-8 1463 ax-10 1464 ax-11 1465 ax-i12 1466 ax-bndl 1467 ax-4 1468 ax-17 1487 ax-i9 1491 ax-ial 1495 ax-i5r 1496 ax-ext 2095 |
This theorem depends on definitions: df-bi 116 df-3an 945 df-tru 1315 df-nf 1418 df-sb 1717 df-clab 2100 df-cleq 2106 df-clel 2109 df-nfc 2242 df-rex 2394 df-v 2657 df-un 3039 df-sn 3497 df-pr 3498 df-op 3500 df-uni 3701 df-br 3894 df-iota 5044 df-fv 5087 df-ov 5729 |
This theorem is referenced by: caov32 5910 oa1suc 6315 nnm1 6372 nnm2 6373 mapsnconst 6540 mapsncnv 6541 mulidnq 7139 halfnqq 7160 addpinq1 7214 addnqpr1 7312 caucvgprlemm 7418 caucvgprprlemval 7438 caucvgprprlemnbj 7443 caucvgprprlemmu 7445 caucvgprprlemaddq 7458 caucvgprprlem1 7459 caucvgprprlem2 7460 m1p1sr 7497 m1m1sr 7498 0idsr 7504 1idsr 7505 00sr 7506 pn0sr 7508 caucvgsrlemoffres 7536 caucvgsr 7538 mulresr 7567 pitonnlem2 7576 axi2m1 7604 ax1rid 7606 axcnre 7610 add42i 7845 negid 7926 negsub 7927 subneg 7928 negsubdii 7964 apreap 8261 recexaplem2 8320 muleqadd 8336 crap0 8620 2p2e4 8745 3p2e5 8759 3p3e6 8760 4p2e6 8761 4p3e7 8762 4p4e8 8763 5p2e7 8764 5p3e8 8765 5p4e9 8766 6p2e8 8767 6p3e9 8768 7p2e9 8769 3t3e9 8775 8th4div3 8837 halfpm6th 8838 iap0 8841 addltmul 8854 div4p1lem1div2 8871 peano2z 8988 nn0n0n1ge2 9019 nneoor 9051 zeo 9054 numsuc 9093 numltc 9105 numsucc 9119 numma 9123 nummul1c 9128 decrmac 9137 decsubi 9142 decmul1 9143 decmul10add 9148 6p5lem 9149 5p5e10 9150 6p4e10 9151 7p3e10 9154 8p2e10 9159 4t3lem 9176 9t11e99 9209 decbin2 9220 fztp 9745 fzprval 9749 fztpval 9750 fzshftral 9775 fz0tp 9788 fzo01 9880 fzo12sn 9881 fzo0to2pr 9882 fzo0to3tp 9883 fzo0to42pr 9884 intqfrac2 9979 intfracq 9980 sqval 10238 sq4e2t8 10277 cu2 10278 i3 10281 i4 10282 binom2i 10288 binom3 10296 3dec 10348 faclbnd 10374 faclbnd2 10375 bcn1 10391 bcn2 10397 4bc3eq4 10406 4bc2eq6 10407 reim0 10520 cji 10561 resqrexlemover 10668 resqrexlemcalc1 10672 resqrexlemcalc3 10674 absi 10717 fsump1i 11088 fsumconst 11109 modfsummodlemstep 11112 arisum2 11154 geoihalfsum 11177 mertenslemi1 11190 mertenslem2 11191 mertensabs 11192 ef0lem 11211 ege2le3 11222 eft0val 11244 ef4p 11245 efgt1p2 11246 efgt1p 11247 tanval2ap 11265 efival 11284 ef01bndlem 11308 sin01bnd 11309 cos01bnd 11310 cos1bnd 11311 cos2bnd 11312 3dvdsdec 11404 3dvds2dec 11405 odd2np1lem 11411 odd2np1 11412 oddp1even 11415 mod2eq1n2dvds 11418 opoe 11434 6gcd4e2 11523 lcmneg 11595 3lcm2e6woprm 11607 6lcm4e12 11608 3prm 11649 3lcm2e6 11678 sqrt2irrlem 11679 pw2dvdslemn 11682 phiprm 11738 restin 12182 uptx 12279 ex-exp 12623 ex-bc 12625 ex-gcd 12627 cvgcmp2nlemabs 12908 |
Copyright terms: Public domain | W3C validator |