MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  oveqan12rd Structured version   Visualization version   GIF version

Theorem oveqan12rd 6898
Description: Equality deduction for operation value. (Contributed by NM, 10-Aug-1995.)
Hypotheses
Ref Expression
oveq1d.1 (𝜑𝐴 = 𝐵)
opreqan12i.2 (𝜓𝐶 = 𝐷)
Assertion
Ref Expression
oveqan12rd ((𝜓𝜑) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))

Proof of Theorem oveqan12rd
StepHypRef Expression
1 oveq1d.1 . . 3 (𝜑𝐴 = 𝐵)
2 opreqan12i.2 . . 3 (𝜓𝐶 = 𝐷)
31, 2oveqan12d 6897 . 2 ((𝜑𝜓) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
43ancoms 451 1 ((𝜓𝜑) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 385   = wceq 1653  (class class class)co 6878
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2777
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-rex 3095  df-rab 3098  df-v 3387  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4116  df-if 4278  df-sn 4369  df-pr 4371  df-op 4375  df-uni 4629  df-br 4844  df-iota 6064  df-fv 6109  df-ov 6881
This theorem is referenced by:  addpipq  10047  mulgt0sr  10214  mulcnsr  10245  mulresr  10248  recdiv  11023  revccat  13846  rlimdiv  14717  caucvg  14750  divgcdcoprm0  15713  estrchom  17081  funcestrcsetclem5  17099  ismhm  17652  mpfrcl  19840  xrsdsval  20112  matval  20542  ucnval  22409  volcn  23714  dvres2lem  24015  dvid  24022  c1lip3  24103  taylthlem1  24468  abelthlem9  24535  brbtwn2  26142  nonbooli  29035  0cnop  29363  0cnfn  29364  idcnop  29365  bccolsum  32139  ftc1anc  33981  rmydioph  38366  expdiophlem2  38374  dvcosax  40885  ismgmhm  42582  2zrngamgm  42738  rnghmsscmap2  42772  rnghmsscmap  42773  funcrngcsetc  42797  rhmsscmap2  42818  rhmsscmap  42819  funcringcsetc  42834
  Copyright terms: Public domain W3C validator