Theorem oveqan12rd 7430

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1568  (class class class)co 7410

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3415  df-v 3455  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-iota 6492  df-fv 6544  df-ov 7413

This theorem is referenced by:  addpipq  10921  mulgt0sr  11089  mulcnsr  11120  mulresr  11123  recdiv  11920  revccat  14802  rlimdiv  15696  caucvg  15729  divgcdcoprm0  16722  estrchom  18182  funcestrcsetclem5  18199  ismgmhm  18753  ismhm  18842  rnghmsscmap2  20713  rnghmsscmap  20714  funcrngcsetc  20724  rhmsscmap2  20742  rhmsscmap  20743  funcringcsetc  20758  xrsdsval  21540  mpfrcl  22215  matval  22547  ucnval  24412  volcn  25744  dvres2lem  26048  dvid  26056  c1lip3  26137  taylthlem1  26512  abelthlem9  26579  2sqnn  27579  brbtwn2  29221  nonbooli  31969  0cnop  32297  0cnfn  32298  idcnop  32299  bccolsum  36185  ftc1anc  38296  rmydioph  43689  expdiophlem2  43697  dvcosax  46588  2zrngamgm  48955