Theorem oveqan12rd 7378

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

Step	Hyp	Ref	Expression
1		oveq1d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2		opreqan12i.2	. . 3 ⊢ (𝜓 → 𝐶 = 𝐷)
3	1, 2	oveqan12d 7377	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
4	3	ancoms 458	1 ⊢ ((𝜓 ∧ 𝜑) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542  (class class class)co 7358

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 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-rab 3399  df-v 3441  df-dif 3903  df-un 3905  df-ss 3917  df-nul 4285  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-iota 6447  df-fv 6499  df-ov 7361

This theorem is referenced by:  addpipq  10850  mulgt0sr  11018  mulcnsr  11049  mulresr  11052  recdiv  11849  revccat  14691  rlimdiv  15571  caucvg  15604  divgcdcoprm0  16594  estrchom  18052  funcestrcsetclem5  18069  ismgmhm  18623  ismhm  18712  rnghmsscmap2  20564  rnghmsscmap  20565  funcrngcsetc  20575  rhmsscmap2  20593  rhmsscmap  20594  funcringcsetc  20609  xrsdsval  21367  mpfrcl  22042  matval  22357  ucnval  24222  volcn  25565  dvres2lem  25869  dvid  25877  c1lip3  25962  taylthlem1  26339  abelthlem9  26408  2sqnn  27408  brbtwn2  28959  nonbooli  31707  0cnop  32035  0cnfn  32036  idcnop  32037  bccolsum  35912  ftc1anc  37871  rmydioph  43293  expdiophlem2  43301  dvcosax  46207  2zrngamgm  48528