Theorem oveqan12rd 7381

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

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

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 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-iota 6449  df-fv 6501  df-ov 7364

This theorem is referenced by:  addpipq  10853  mulgt0sr  11021  mulcnsr  11052  mulresr  11055  recdiv  11852  revccat  14694  rlimdiv  15574  caucvg  15607  divgcdcoprm0  16597  estrchom  18055  funcestrcsetclem5  18072  ismgmhm  18626  ismhm  18715  rnghmsscmap2  20567  rnghmsscmap  20568  funcrngcsetc  20578  rhmsscmap2  20596  rhmsscmap  20597  funcringcsetc  20612  xrsdsval  21370  mpfrcl  22045  matval  22360  ucnval  24225  volcn  25568  dvres2lem  25872  dvid  25880  c1lip3  25965  taylthlem1  26342  abelthlem9  26411  2sqnn  27411  brbtwn2  28983  nonbooli  31731  0cnop  32059  0cnfn  32060  idcnop  32061  bccolsum  35946  ftc1anc  37915  rmydioph  43334  expdiophlem2  43342  dvcosax  46247  2zrngamgm  48568