Theorem oveqan12rd 7431

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541  (class class class)co 7411

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6495  df-fv 6551  df-ov 7414

This theorem is referenced by:  addpipq  10934  mulgt0sr  11102  mulcnsr  11133  mulresr  11136  recdiv  11922  revccat  14718  rlimdiv  15594  caucvg  15627  divgcdcoprm0  16604  estrchom  18080  funcestrcsetclem5  18098  ismhm  18675  xrsdsval  20995  mpfrcl  21654  matval  21918  ucnval  23789  volcn  25130  dvres2lem  25434  dvid  25442  c1lip3  25523  taylthlem1  25892  abelthlem9  25959  2sqnn  26949  brbtwn2  28201  nonbooli  30942  0cnop  31270  0cnfn  31271  idcnop  31272  bccolsum  34778  ftc1anc  36655  rmydioph  41835  expdiophlem2  41843  dvcosax  44721  ismgmhm  46632  2zrngamgm  46916  rnghmsscmap2  46950  rnghmsscmap  46951  funcrngcsetc  46975  rhmsscmap2  46996  rhmsscmap  46997  funcringcsetc  47012