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

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

Proof of Theorem oveq12
StepHypRef Expression
1 oveq1 5747 . 2 (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))
2 oveq2 5748 . 2 (𝐶 = 𝐷 → (𝐵𝐹𝐶) = (𝐵𝐹𝐷))
31, 2sylan9eq 2168 1 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103   = wceq 1314  (class class class)co 5740
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-3an 947  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-rex 2397  df-v 2660  df-un 3043  df-sn 3501  df-pr 3502  df-op 3504  df-uni 3705  df-br 3898  df-iota 5056  df-fv 5099  df-ov 5743
This theorem is referenced by:  oveq12i  5752  oveq12d  5758  oveqan12d  5759  ecopoveq  6490  ecopovtrn  6492  ecopovtrng  6495  th3qlem1  6497  th3qlem2  6498  mulcmpblnq  7140  addpipqqs  7142  ordpipqqs  7146  enq0breq  7208  mulcmpblnq0  7216  nqpnq0nq  7225  nqnq0a  7226  nqnq0m  7227  nq0m0r  7228  nq0a0  7229  distrlem5prl  7358  distrlem5pru  7359  addcmpblnr  7511  ltsrprg  7519  mulgt0sr  7550  add20  8200  cru  8327  qaddcl  9376  qmulcl  9378  xaddval  9568  xnn0xadd0  9590  fzopth  9781  modqval  10037  seqvalcd  10172  seqovcd  10176  1exp  10262  m1expeven  10280  nn0opthd  10408  faclbnd  10427  faclbnd3  10429  bcn0  10441  reval  10561  absval  10713  clim  10990  fsumparts  11179  dvds2add  11423  dvds2sub  11424  opoe  11488  omoe  11489  opeo  11490  omeo  11491  gcddvds  11548  gcdcl  11551  gcdeq0  11561  gcdneg  11566  gcdaddm  11568  gcdabs  11572  gcddiv  11603  eucalgval2  11630  lcmabs  11653  rpmul  11675  divgcdcoprmex  11679  prmexpb  11725  rpexp  11727  nn0gcdsq  11773  cnmpt2t  12357  cnmpt22f  12359  hmeofvalg  12367  bdmetval  12564
  Copyright terms: Public domain W3C validator