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

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

Proof of Theorem oveq12
StepHypRef Expression
1 oveq1 5641 . 2 (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))
2 oveq2 5642 . 2 (𝐶 = 𝐷 → (𝐵𝐹𝐶) = (𝐵𝐹𝐷))
31, 2sylan9eq 2140 1 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102   = wceq 1289  (class class class)co 5634
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070
This theorem depends on definitions:  df-bi 115  df-3an 926  df-tru 1292  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-rex 2365  df-v 2621  df-un 3001  df-sn 3447  df-pr 3448  df-op 3450  df-uni 3649  df-br 3838  df-iota 4967  df-fv 5010  df-ov 5637
This theorem is referenced by:  oveq12i  5646  oveq12d  5652  oveqan12d  5653  sprmpt2  5989  ecopoveq  6367  ecopovtrn  6369  ecopovtrng  6372  th3qlem1  6374  th3qlem2  6375  mulcmpblnq  6906  addpipqqs  6908  ordpipqqs  6912  enq0breq  6974  mulcmpblnq0  6982  nqpnq0nq  6991  nqnq0a  6992  nqnq0m  6993  nq0m0r  6994  nq0a0  6995  distrlem5prl  7124  distrlem5pru  7125  addcmpblnr  7264  ltsrprg  7272  mulgt0sr  7302  add20  7931  cru  8055  qaddcl  9089  qmulcl  9091  fzopth  9443  modqval  9696  1exp  9949  m1expeven  9967  nn0opthd  10095  faclbnd  10114  faclbnd3  10116  bcn0  10128  reval  10248  absval  10399  clim  10633  fsumparts  10827  dvds2add  10923  dvds2sub  10924  opoe  10988  omoe  10989  opeo  10990  omeo  10991  gcddvds  11048  gcdcl  11051  gcdeq0  11061  gcdneg  11066  gcdaddm  11068  gcdabs  11072  gcddiv  11101  eucalgval2  11128  lcmabs  11151  rpmul  11173  divgcdcoprmex  11177  prmexpb  11223  rpexp  11225  nn0gcdsq  11271
  Copyright terms: Public domain W3C validator