Theorem oveqan12rd 7434

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539  (class class class)co 7414

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-rab 3421  df-v 3466  df-dif 3936  df-un 3938  df-ss 3950  df-nul 4316  df-if 4508  df-sn 4609  df-pr 4611  df-op 4615  df-uni 4890  df-br 5126  df-iota 6495  df-fv 6550  df-ov 7417

This theorem is referenced by:  addpipq  10960  mulgt0sr  11128  mulcnsr  11159  mulresr  11162  recdiv  11956  revccat  14787  rlimdiv  15665  caucvg  15698  divgcdcoprm0  16685  estrchom  18147  funcestrcsetclem5  18164  ismgmhm  18683  ismhm  18772  rnghmsscmap2  20602  rnghmsscmap  20603  funcrngcsetc  20613  rhmsscmap2  20631  rhmsscmap  20632  funcringcsetc  20647  xrsdsval  21395  mpfrcl  22076  matval  22382  ucnval  24250  volcn  25596  dvres2lem  25900  dvid  25908  c1lip3  25993  taylthlem1  26370  abelthlem9  26439  2sqnn  27438  brbtwn2  28869  nonbooli  31617  0cnop  31945  0cnfn  31946  idcnop  31947  bccolsum  35680  ftc1anc  37649  rmydioph  42971  expdiophlem2  42979  dvcosax  45886  2zrngamgm  48107