Theorem oveqan12rd 7155

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538  (class class class)co 7135

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-iota 6283  df-fv 6332  df-ov 7138

This theorem is referenced by:  addpipq  10348  mulgt0sr  10516  mulcnsr  10547  mulresr  10550  recdiv  11335  revccat  14119  rlimdiv  14994  caucvg  15027  divgcdcoprm0  15999  estrchom  17369  funcestrcsetclem5  17386  ismhm  17950  xrsdsval  20135  mpfrcl  20757  matval  21016  ucnval  22883  volcn  24210  dvres2lem  24513  dvid  24521  c1lip3  24602  taylthlem1  24968  abelthlem9  25035  2sqnn  26023  brbtwn2  26699  nonbooli  29434  0cnop  29762  0cnfn  29763  idcnop  29764  bccolsum  33084  ftc1anc  35138  rmydioph  39955  expdiophlem2  39963  dvcosax  42568  ismgmhm  44403  2zrngamgm  44563  rnghmsscmap2  44597  rnghmsscmap  44598  funcrngcsetc  44622  rhmsscmap2  44643  rhmsscmap  44644  funcringcsetc  44659