Theorem oveqan12rd 7432

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   = wceq 1569  (class class class)co 7412

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3416  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-iota 6492  df-fv 6544  df-ov 7415

This theorem is used by:  addpipq  10928  mulgt0sr  11096  mulcnsr  11127  mulresr  11130  recdiv  11927  revccat  14810  rlimdiv  15704  caucvg  15737  divgcdcoprm0  16729  estrchom  18189  funcestrcsetclem5  18206  ismgmhm  18760  ismhm  18849  rnghmsscmap2  20739  rnghmsscmap  20740  funcrngcsetc  20750  rhmsscmap2  20768  rhmsscmap  20769  funcringcsetc  20784  xrsdsval  21572  mpfrcl  22247  matval  22579  ucnval  24444  volcn  25776  dvres2lem  26080  dvid  26088  c1lip3  26169  taylthlem1  26547  abelthlem9  26614  2sqnn  27614  brbtwn2  29266  nonbooli  32014  0cnop  32342  0cnfn  32343  idcnop  32344  bccolsum  36239  ftc1anc  38380  rmydioph  43769  expdiophlem2  43777  dvcosax  46668  2zrngamgm  49038