Theorem oveqan12rd 7380

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

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1548  (class class class)co 7360

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-rab 3394  df-v 3435  df-dif 3888  df-un 3890  df-ss 3902  df-nul 4265  df-if 4458  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4842  df-br 5076  df-iota 6445  df-fv 6497  df-ov 7363

This theorem is referenced by:  addpipq  10855  mulgt0sr  11023  mulcnsr  11054  mulresr  11057  recdiv  11856  revccat  14723  rlimdiv  15603  caucvg  15636  divgcdcoprm0  16629  estrchom  18088  funcestrcsetclem5  18105  ismgmhm  18659  ismhm  18748  rnghmsscmap2  20605  rnghmsscmap  20606  funcrngcsetc  20616  rhmsscmap2  20634  rhmsscmap  20635  funcringcsetc  20650  xrsdsval  21390  mpfrcl  22065  matval  22398  ucnval  24263  volcn  25595  dvres2lem  25899  dvid  25907  c1lip3  25988  taylthlem1  26360  abelthlem9  26427  2sqnn  27424  brbtwn2  28996  nonbooli  31744  0cnop  32072  0cnfn  32073  idcnop  32074  bccolsum  35982  ftc1anc  38083  rmydioph  43474  expdiophlem2  43482  dvcosax  46383  2zrngamgm  48750