Theorem oveqan12rd 7418

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1562  (class class class)co 7398

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-rab 3417  df-v 3458  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5103  df-iota 6479  df-fv 6531  df-ov 7401

This theorem is referenced by:  addpipq  10897  mulgt0sr  11065  mulcnsr  11096  mulresr  11099  recdiv  11899  revccat  14781  rlimdiv  15675  caucvg  15708  divgcdcoprm0  16701  estrchom  18161  funcestrcsetclem5  18178  ismgmhm  18732  ismhm  18821  rnghmsscmap2  20681  rnghmsscmap  20682  funcrngcsetc  20692  rhmsscmap2  20710  rhmsscmap  20711  funcringcsetc  20726  xrsdsval  21465  mpfrcl  22140  matval  22473  ucnval  24338  volcn  25670  dvres2lem  25974  dvid  25982  c1lip3  26063  taylthlem1  26438  abelthlem9  26505  2sqnn  27505  brbtwn2  29108  nonbooli  31856  0cnop  32184  0cnfn  32185  idcnop  32186  bccolsum  36094  ftc1anc  38205  rmydioph  43596  expdiophlem2  43604  dvcosax  46505  2zrngamgm  48872