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

Theorem oveqan12rd 6630
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 6629 . 2 ((𝜑𝜓) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
43ancoms 469 1 ((𝜓𝜑) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1480  (class class class)co 6610
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rex 2913  df-rab 2916  df-v 3191  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-nul 3897  df-if 4064  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-br 4619  df-iota 5815  df-fv 5860  df-ov 6613
This theorem is referenced by:  addpipq  9711  mulgt0sr  9878  mulcnsr  9909  mulresr  9912  recdiv  10683  revccat  13460  rlimdiv  14318  caucvg  14351  divgcdcoprm0  15314  estrchom  16699  funcestrcsetclem5  16716  ismhm  17269  mpfrcl  19450  xrsdsval  19722  matval  20149  ucnval  22004  volcn  23297  dvres2lem  23597  dvid  23604  c1lip3  23683  taylthlem1  24048  abelthlem9  24115  brbtwn2  25702  nonbooli  28380  0cnop  28708  0cnfn  28709  idcnop  28710  bccolsum  31368  ftc1anc  33160  rmydioph  37096  expdiophlem2  37104  dvcosax  39474  ismgmhm  41097  2zrngamgm  41253  rnghmsscmap2  41287  rnghmsscmap  41288  funcrngcsetc  41312  rhmsscmap2  41333  rhmsscmap  41334  funcringcsetc  41349
  Copyright terms: Public domain W3C validator