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

Theorem oveq12 5548
Description: Equality theorem for operation value. (Contributed by NM, 16-Jul-1995.)
Assertion
Ref Expression
oveq12 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))

Proof of Theorem oveq12
StepHypRef Expression
1 oveq1 5546 . 2 (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))
2 oveq2 5547 . 2 (𝐶 = 𝐷 → (𝐵𝐹𝐶) = (𝐵𝐹𝐷))
31, 2sylan9eq 2108 1 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101   = wceq 1259  (class class class)co 5539
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-3an 898  df-tru 1262  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-rex 2329  df-v 2576  df-un 2949  df-sn 3408  df-pr 3409  df-op 3411  df-uni 3608  df-br 3792  df-iota 4894  df-fv 4937  df-ov 5542
This theorem is referenced by:  oveq12i  5551  oveq12d  5557  oveqan12d  5558  sprmpt2  5887  ecopoveq  6231  ecopovtrn  6233  ecopovtrng  6236  th3qlem1  6238  th3qlem2  6239  mulcmpblnq  6523  addpipqqs  6525  ordpipqqs  6529  enq0breq  6591  mulcmpblnq0  6599  nqpnq0nq  6608  nqnq0a  6609  nqnq0m  6610  nq0m0r  6611  nq0a0  6612  distrlem5prl  6741  distrlem5pru  6742  addcmpblnr  6881  ltsrprg  6889  mulgt0sr  6919  add20  7542  cru  7666  qaddcl  8666  qmulcl  8668  fzopth  9025  modqval  9268  1exp  9443  m1expeven  9461  nn0opthd  9583  faclbnd  9602  faclbnd3  9604  bcn0  9616  reval  9670  absval  9820  clim  10025  dvds2add  10133  dvds2sub  10134  opoe  10199  omoe  10200  opeo  10201  omeo  10202
  Copyright terms: Public domain W3C validator