Theorem oveqan12rd 7389

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

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

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-iota 6452  df-fv 6507  df-ov 7372

This theorem is referenced by:  addpipq  10868  mulgt0sr  11036  mulcnsr  11067  mulresr  11070  recdiv  11866  revccat  14708  rlimdiv  15589  caucvg  15622  divgcdcoprm0  16612  estrchom  18069  funcestrcsetclem5  18086  ismgmhm  18606  ismhm  18695  rnghmsscmap2  20550  rnghmsscmap  20551  funcrngcsetc  20561  rhmsscmap2  20579  rhmsscmap  20580  funcringcsetc  20595  xrsdsval  21353  mpfrcl  22026  matval  22332  ucnval  24198  volcn  25541  dvres2lem  25845  dvid  25853  c1lip3  25938  taylthlem1  26315  abelthlem9  26384  2sqnn  27384  brbtwn2  28886  nonbooli  31631  0cnop  31959  0cnfn  31960  idcnop  31961  bccolsum  35720  ftc1anc  37689  rmydioph  42997  expdiophlem2  43005  dvcosax  45918  2zrngamgm  48227