Theorem oveqan12rd 7430

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

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

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 2708

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 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-iota 6489  df-fv 6544  df-ov 7413

This theorem is referenced by:  addpipq  10956  mulgt0sr  11124  mulcnsr  11155  mulresr  11158  recdiv  11952  revccat  14789  rlimdiv  15667  caucvg  15700  divgcdcoprm0  16689  estrchom  18144  funcestrcsetclem5  18161  ismgmhm  18679  ismhm  18768  rnghmsscmap2  20594  rnghmsscmap  20595  funcrngcsetc  20605  rhmsscmap2  20623  rhmsscmap  20624  funcringcsetc  20639  xrsdsval  21383  mpfrcl  22048  matval  22354  ucnval  24220  volcn  25564  dvres2lem  25868  dvid  25876  c1lip3  25961  taylthlem1  26338  abelthlem9  26407  2sqnn  27407  brbtwn2  28889  nonbooli  31637  0cnop  31965  0cnfn  31966  idcnop  31967  bccolsum  35761  ftc1anc  37730  rmydioph  43013  expdiophlem2  43021  dvcosax  45935  2zrngamgm  48200