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

Theorem oveqan12rd 7165
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 7164 . 2 ((𝜑𝜓) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
43ancoms 459 1 ((𝜓𝜑) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1528  (class class class)co 7145
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rex 3141  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-iota 6307  df-fv 6356  df-ov 7148
This theorem is referenced by:  addpipq  10347  mulgt0sr  10515  mulcnsr  10546  mulresr  10549  recdiv  11334  revccat  14116  rlimdiv  14990  caucvg  15023  divgcdcoprm0  15997  estrchom  17365  funcestrcsetclem5  17382  ismhm  17946  mpfrcl  20226  xrsdsval  20517  matval  20948  ucnval  22813  volcn  24134  dvres2lem  24435  dvid  24442  c1lip3  24523  taylthlem1  24888  abelthlem9  24955  2sqnn  25942  brbtwn2  26618  nonbooli  29355  0cnop  29683  0cnfn  29684  idcnop  29685  bccolsum  32868  ftc1anc  34856  rmydioph  39489  expdiophlem2  39497  dvcosax  42087  ismgmhm  43927  2zrngamgm  44138  rnghmsscmap2  44172  rnghmsscmap  44173  funcrngcsetc  44197  rhmsscmap2  44218  rhmsscmap  44219  funcringcsetc  44234
  Copyright terms: Public domain W3C validator