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

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

Proof of Theorem oveq12
StepHypRef Expression
1 oveq1 5571 . 2 (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))
2 oveq2 5572 . 2 (𝐶 = 𝐷 → (𝐵𝐹𝐶) = (𝐵𝐹𝐷))
31, 2sylan9eq 2135 1 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102   = wceq 1285  (class class class)co 5564
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 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065
This theorem depends on definitions:  df-bi 115  df-3an 922  df-tru 1288  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-rex 2359  df-v 2612  df-un 2987  df-sn 3423  df-pr 3424  df-op 3426  df-uni 3623  df-br 3807  df-iota 4918  df-fv 4961  df-ov 5567
This theorem is referenced by:  oveq12i  5576  oveq12d  5582  oveqan12d  5583  sprmpt2  5912  ecopoveq  6289  ecopovtrn  6291  ecopovtrng  6294  th3qlem1  6296  th3qlem2  6297  mulcmpblnq  6656  addpipqqs  6658  ordpipqqs  6662  enq0breq  6724  mulcmpblnq0  6732  nqpnq0nq  6741  nqnq0a  6742  nqnq0m  6743  nq0m0r  6744  nq0a0  6745  distrlem5prl  6874  distrlem5pru  6875  addcmpblnr  7014  ltsrprg  7022  mulgt0sr  7052  add20  7681  cru  7805  qaddcl  8837  qmulcl  8839  fzopth  9191  modqval  9442  1exp  9638  m1expeven  9656  nn0opthd  9782  faclbnd  9801  faclbnd3  9803  bcn0  9815  reval  9921  absval  10072  clim  10305  dvds2add  10421  dvds2sub  10422  opoe  10486  omoe  10487  opeo  10488  omeo  10489  gcddvds  10546  gcdcl  10549  gcdeq0  10559  gcdneg  10564  gcdaddm  10566  gcdabs  10570  gcddiv  10599  eucalgval2  10626  lcmabs  10649  rpmul  10671  divgcdcoprmex  10675  prmexpb  10721  rpexp  10723  nn0gcdsq  10769
  Copyright terms: Public domain W3C validator