Theorem oveqan12rd 7436

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

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

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 2734

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 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-iota 6493  df-fv 6545  df-ov 7419

This theorem is used by:  addpipq  10949  mulgt0sr  11117  mulcnsr  11148  mulresr  11151  recdiv  11948  revccat  14837  rlimdiv  15735  caucvg  15768  divgcdcoprm0  16759  estrchom  18219  funcestrcsetclem5  18236  ismgmhm  18800  ismhm  18894  rnghmsscmap2  20792  rnghmsscmap  20793  funcrngcsetc  20803  rhmsscmap2  20821  rhmsscmap  20822  funcringcsetc  20837  xrsdsval  21625  mpfrcl  22302  matval  22634  ucnval  24503  volcn  25835  dvres2lem  26139  dvid  26147  c1lip3  26228  taylthlem1  26606  abelthlem9  26673  2sqnn  27673  brbtwn2  29348  nonbooli  32118  0cnop  32446  0cnfn  32447  idcnop  32448  bccolsum  36305  ftc1anc  38437  rmydioph  43842  expdiophlem2  43850  dvcosax  46741  2zrngamgm  49147