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

Theorem oveqan12rd 7158
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 7157 . 2 ((𝜑𝜓) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
43ancoms 462 1 ((𝜓𝜑) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399   = wceq 1538  (class class class)co 7138
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-rab 3141  df-v 3481  df-dif 3921  df-un 3923  df-in 3925  df-ss 3935  df-nul 4275  df-if 4449  df-sn 4549  df-pr 4551  df-op 4555  df-uni 4820  df-br 5048  df-iota 6295  df-fv 6344  df-ov 7141
This theorem is referenced by:  addpipq  10344  mulgt0sr  10512  mulcnsr  10543  mulresr  10546  recdiv  11331  revccat  14117  rlimdiv  14991  caucvg  15024  divgcdcoprm0  15996  estrchom  17366  funcestrcsetclem5  17383  ismhm  17947  mpfrcl  20284  xrsdsval  20575  matval  21006  ucnval  22872  volcn  24199  dvres2lem  24502  dvid  24510  c1lip3  24591  taylthlem1  24957  abelthlem9  25024  2sqnn  26012  brbtwn2  26688  nonbooli  29423  0cnop  29751  0cnfn  29752  idcnop  29753  bccolsum  32989  ftc1anc  35038  rmydioph  39787  expdiophlem2  39795  dvcosax  42410  ismgmhm  44245  2zrngamgm  44405  rnghmsscmap2  44439  rnghmsscmap  44440  funcrngcsetc  44464  rhmsscmap2  44485  rhmsscmap  44486  funcringcsetc  44501
  Copyright terms: Public domain W3C validator