Theorem oveqan12rd 7369

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 7368	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
4	3	ancoms 458	1 ⊢ ((𝜓 ∧ 𝜑) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540  (class class class)co 7349

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-iota 6438  df-fv 6490  df-ov 7352

This theorem is referenced by:  addpipq  10831  mulgt0sr  10999  mulcnsr  11030  mulresr  11033  recdiv  11830  revccat  14672  rlimdiv  15553  caucvg  15586  divgcdcoprm0  16576  estrchom  18033  funcestrcsetclem5  18050  ismgmhm  18570  ismhm  18659  rnghmsscmap2  20514  rnghmsscmap  20515  funcrngcsetc  20525  rhmsscmap2  20543  rhmsscmap  20544  funcringcsetc  20559  xrsdsval  21317  mpfrcl  21990  matval  22296  ucnval  24162  volcn  25505  dvres2lem  25809  dvid  25817  c1lip3  25902  taylthlem1  26279  abelthlem9  26348  2sqnn  27348  brbtwn2  28854  nonbooli  31599  0cnop  31927  0cnfn  31928  idcnop  31929  bccolsum  35732  ftc1anc  37701  rmydioph  43007  expdiophlem2  43015  dvcosax  45927  2zrngamgm  48249