ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  oveq1i GIF version

Theorem oveq1i 5522
Description: Equality inference for operation value. (Contributed by NM, 28-Feb-1995.)
Hypothesis
Ref Expression
oveq1i.1 𝐴 = 𝐵
Assertion
Ref Expression
oveq1i (𝐴𝐹𝐶) = (𝐵𝐹𝐶)

Proof of Theorem oveq1i
StepHypRef Expression
1 oveq1i.1 . 2 𝐴 = 𝐵
2 oveq1 5519 . 2 (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))
31, 2ax-mp 7 1 (𝐴𝐹𝐶) = (𝐵𝐹𝐶)
Colors of variables: wff set class
Syntax hints:   = wceq 1243  (class class class)co 5512
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-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022
This theorem depends on definitions:  df-bi 110  df-3an 887  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-rex 2312  df-v 2559  df-un 2922  df-sn 3381  df-pr 3382  df-op 3384  df-uni 3581  df-br 3765  df-iota 4867  df-fv 4910  df-ov 5515
This theorem is referenced by:  caov12  5689  halfnqq  6506  prarloclem5  6596  m1m1sr  6844  caucvgsrlemfv  6873  caucvgsr  6884  pitonnlem1  6919  axi2m1  6947  axcnre  6953  axcaucvg  6972  mvrraddi  7226  mvlladdi  7227  negsubdi  7265  mul02  7382  mulneg1  7390  mulreim  7593  recextlem1  7630  recdivap  7692  2p2e4  8035  2times  8036  3p2e5  8050  3p3e6  8051  4p2e6  8052  4p3e7  8053  4p4e8  8054  5p2e7  8055  5p3e8  8056  5p4e9  8057  5p5e10  8058  6p2e8  8059  6p3e9  8060  6p4e10  8061  7p2e9  8062  7p3e10  8063  8p2e10  8064  1mhlfehlf  8141  8th4div3  8142  halfpm6th  8143  nneoor  8338  num0h  8375  numsuc  8377  dec10p  8394  numma  8396  nummac  8397  numma2c  8398  numadd  8399  numaddc  8400  nummul2c  8402  decaddci  8410  decbin0  8468  decbin2  8469  elfzp1b  8957  elfzm1b  8958  qbtwnrelemcalc  9108  fldiv4p1lem1div2  9145  mulexpzap  9293  expaddzap  9297  cu2  9349  i3  9352  binom2i  9358  binom3  9364  imre  9449  crim  9456  remullem  9469  resqrexlemfp1  9605  resqrexlemover  9606  resqrexlemcalc1  9610  resqrexlemnm  9614  absexpzap  9674  absimle  9678  amgm2  9712  ex-fl  9893  qdencn  10121
  Copyright terms: Public domain W3C validator