Theorem oveqan12rd 7387

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542  (class class class)co 7367

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6455  df-fv 6507  df-ov 7370

This theorem is referenced by:  addpipq  10860  mulgt0sr  11028  mulcnsr  11059  mulresr  11062  recdiv  11861  revccat  14728  rlimdiv  15608  caucvg  15641  divgcdcoprm0  16634  estrchom  18093  funcestrcsetclem5  18110  ismgmhm  18664  ismhm  18753  rnghmsscmap2  20606  rnghmsscmap  20607  funcrngcsetc  20617  rhmsscmap2  20635  rhmsscmap  20636  funcringcsetc  20651  xrsdsval  21391  mpfrcl  22063  matval  22376  ucnval  24241  volcn  25573  dvres2lem  25877  dvid  25885  c1lip3  25966  taylthlem1  26338  abelthlem9  26405  2sqnn  27402  brbtwn2  28974  nonbooli  31722  0cnop  32050  0cnfn  32051  idcnop  32052  bccolsum  35921  ftc1anc  38022  rmydioph  43442  expdiophlem2  43450  dvcosax  46354  2zrngamgm  48715