Theorem oveqan12rd 7407

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540  (class class class)co 7387

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390

This theorem is referenced by:  addpipq  10890  mulgt0sr  11058  mulcnsr  11089  mulresr  11092  recdiv  11888  revccat  14731  rlimdiv  15612  caucvg  15645  divgcdcoprm0  16635  estrchom  18088  funcestrcsetclem5  18105  ismgmhm  18623  ismhm  18712  rnghmsscmap2  20538  rnghmsscmap  20539  funcrngcsetc  20549  rhmsscmap2  20567  rhmsscmap  20568  funcringcsetc  20583  xrsdsval  21327  mpfrcl  21992  matval  22298  ucnval  24164  volcn  25507  dvres2lem  25811  dvid  25819  c1lip3  25904  taylthlem1  26281  abelthlem9  26350  2sqnn  27350  brbtwn2  28832  nonbooli  31580  0cnop  31908  0cnfn  31909  idcnop  31910  bccolsum  35726  ftc1anc  37695  rmydioph  43003  expdiophlem2  43011  dvcosax  45924  2zrngamgm  48233