Theorem oveqan12rd 7382

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

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

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 2702

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 2709  df-cleq 2723  df-clel 2809  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-iota 6453  df-fv 6509  df-ov 7365

This theorem is referenced by:  addpipq  10882  mulgt0sr  11050  mulcnsr  11081  mulresr  11084  recdiv  11870  revccat  14666  rlimdiv  15542  caucvg  15575  divgcdcoprm0  16552  estrchom  18028  funcestrcsetclem5  18046  ismhm  18617  xrsdsval  20878  mpfrcl  21532  matval  21795  ucnval  23666  volcn  25007  dvres2lem  25311  dvid  25319  c1lip3  25400  taylthlem1  25769  abelthlem9  25836  2sqnn  26824  brbtwn2  27917  nonbooli  30656  0cnop  30984  0cnfn  30985  idcnop  30986  bccolsum  34398  ftc1anc  36232  rmydioph  41396  expdiophlem2  41404  dvcosax  44287  ismgmhm  46197  2zrngamgm  46357  rnghmsscmap2  46391  rnghmsscmap  46392  funcrngcsetc  46416  rhmsscmap2  46437  rhmsscmap  46438  funcringcsetc  46453