Theorem oveqan12rd 7289

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1542  (class class class)co 7269

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-rab 3075  df-v 3433  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4846  df-br 5080  df-iota 6389  df-fv 6439  df-ov 7272

This theorem is referenced by:  addpipq  10692  mulgt0sr  10860  mulcnsr  10891  mulresr  10894  recdiv  11679  revccat  14475  rlimdiv  15353  caucvg  15386  divgcdcoprm0  16366  estrchom  17839  funcestrcsetclem5  17857  ismhm  18428  xrsdsval  20638  mpfrcl  21291  matval  21554  ucnval  23425  volcn  24766  dvres2lem  25070  dvid  25078  c1lip3  25159  taylthlem1  25528  abelthlem9  25595  2sqnn  26583  brbtwn2  27269  nonbooli  30007  0cnop  30335  0cnfn  30336  idcnop  30337  bccolsum  33699  ftc1anc  35852  rmydioph  40831  expdiophlem2  40839  dvcosax  43436  ismgmhm  45304  2zrngamgm  45464  rnghmsscmap2  45498  rnghmsscmap  45499  funcrngcsetc  45523  rhmsscmap2  45544  rhmsscmap  45545  funcringcsetc  45560