Theorem oveqan12rd 7428

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570  (class class class)co 7408

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-iota 6483  df-fv 6535  df-ov 7411

This theorem is used by:  addpipq  10993  mulgt0sr  11161  mulcnsr  11192  mulresr  11195  recdiv  11992  revccat  14882  rlimdiv  15780  caucvg  15813  divgcdcoprm0  16802  estrchom  18262  funcestrcsetclem5  18279  ismgmhm  18846  ismhm  18941  rnghmsscmap2  20842  rnghmsscmap  20843  funcrngcsetc  20853  rhmsscmap2  20871  rhmsscmap  20872  funcringcsetc  20887  xrsdsval  21678  mpfrcl  22355  matval  22687  ucnval  24556  volcn  25888  dvres2lem  26191  dvid  26199  c1lip3  26280  taylthlem1  26663  abelthlem9  26730  2sqnn  27729  brbtwn2  29416  nonbooli  32186  0cnop  32514  0cnfn  32515  idcnop  32516  bccolsum  36425  ftc1anc  38539  rmydioph  43959  expdiophlem2  43967  dvcosax  46858  2zrngamgm  49264