Theorem oveqan12rd 7421

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1533  (class class class)co 7401

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-rab 3425  df-v 3468  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-nul 4315  df-if 4521  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-br 5139  df-iota 6485  df-fv 6541  df-ov 7404

This theorem is referenced by:  addpipq  10927  mulgt0sr  11095  mulcnsr  11126  mulresr  11129  recdiv  11916  revccat  14712  rlimdiv  15588  caucvg  15621  divgcdcoprm0  16598  estrchom  18077  funcestrcsetclem5  18095  ismgmhm  18616  ismhm  18702  rnghmsscmap2  20510  rnghmsscmap  20511  funcrngcsetc  20521  rhmsscmap2  20539  rhmsscmap  20540  funcringcsetc  20555  xrsdsval  21268  mpfrcl  21949  matval  22221  ucnval  24092  volcn  25445  dvres2lem  25749  dvid  25757  c1lip3  25842  taylthlem1  26214  abelthlem9  26282  2sqnn  27276  brbtwn2  28587  nonbooli  31328  0cnop  31656  0cnfn  31657  idcnop  31658  bccolsum  35170  ftc1anc  37025  rmydioph  42208  expdiophlem2  42216  dvcosax  45093  2zrngamgm  47074