Theorem oveqan12rd 7295

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539  (class class class)co 7275

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-iota 6391  df-fv 6441  df-ov 7278

This theorem is referenced by:  addpipq  10693  mulgt0sr  10861  mulcnsr  10892  mulresr  10895  recdiv  11681  revccat  14479  rlimdiv  15357  caucvg  15390  divgcdcoprm0  16370  estrchom  17843  funcestrcsetclem5  17861  ismhm  18432  xrsdsval  20642  mpfrcl  21295  matval  21558  ucnval  23429  volcn  24770  dvres2lem  25074  dvid  25082  c1lip3  25163  taylthlem1  25532  abelthlem9  25599  2sqnn  26587  brbtwn2  27273  nonbooli  30013  0cnop  30341  0cnfn  30342  idcnop  30343  bccolsum  33705  ftc1anc  35858  rmydioph  40836  expdiophlem2  40844  dvcosax  43467  ismgmhm  45337  2zrngamgm  45497  rnghmsscmap2  45531  rnghmsscmap  45532  funcrngcsetc  45556  rhmsscmap2  45577  rhmsscmap  45578  funcringcsetc  45593