Theorem oveqan12rd 7390

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

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

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 6453  df-fv 6508  df-ov 7373

This theorem is referenced by:  addpipq  10869  mulgt0sr  11037  mulcnsr  11068  mulresr  11071  recdiv  11867  revccat  14709  rlimdiv  15590  caucvg  15623  divgcdcoprm0  16613  estrchom  18070  funcestrcsetclem5  18087  ismgmhm  18607  ismhm  18696  rnghmsscmap2  20551  rnghmsscmap  20552  funcrngcsetc  20562  rhmsscmap2  20580  rhmsscmap  20581  funcringcsetc  20596  xrsdsval  21354  mpfrcl  22027  matval  22333  ucnval  24199  volcn  25542  dvres2lem  25846  dvid  25854  c1lip3  25939  taylthlem1  26316  abelthlem9  26385  2sqnn  27385  brbtwn2  28887  nonbooli  31632  0cnop  31960  0cnfn  31961  idcnop  31962  bccolsum  35721  ftc1anc  37690  rmydioph  42998  expdiophlem2  43006  dvcosax  45919  2zrngamgm  48228