Theorem oveqan12rd 7378

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542  (class class class)co 7358

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6446  df-fv 6498  df-ov 7361

This theorem is referenced by:  addpipq  10849  mulgt0sr  11017  mulcnsr  11048  mulresr  11051  recdiv  11848  revccat  14690  rlimdiv  15570  caucvg  15603  divgcdcoprm0  16593  estrchom  18051  funcestrcsetclem5  18068  ismgmhm  18622  ismhm  18711  rnghmsscmap2  20564  rnghmsscmap  20565  funcrngcsetc  20575  rhmsscmap2  20593  rhmsscmap  20594  funcringcsetc  20609  xrsdsval  21367  mpfrcl  22041  matval  22354  ucnval  24219  volcn  25551  dvres2lem  25855  dvid  25863  c1lip3  25945  taylthlem1  26321  abelthlem9  26390  2sqnn  27390  brbtwn2  28962  nonbooli  31711  0cnop  32039  0cnfn  32040  idcnop  32041  bccolsum  35927  ftc1anc  38013  rmydioph  43445  expdiophlem2  43453  dvcosax  46358  2zrngamgm  48679