Theorem oveqan12rd 6834

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

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1632  (class class class)co 6814

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rex 3056  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-iota 6012  df-fv 6057  df-ov 6817

This theorem is referenced by:  addpipq  9971  mulgt0sr  10138  mulcnsr  10169  mulresr  10172  recdiv  10943  revccat  13735  rlimdiv  14595  caucvg  14628  divgcdcoprm0  15601  estrchom  16988  funcestrcsetclem5  17005  ismhm  17558  mpfrcl  19740  xrsdsval  20012  matval  20439  ucnval  22302  volcn  23594  dvres2lem  23893  dvid  23900  c1lip3  23981  taylthlem1  24346  abelthlem9  24413  brbtwn2  26005  nonbooli  28840  0cnop  29168  0cnfn  29169  idcnop  29170  bccolsum  31953  ftc1anc  33824  rmydioph  38101  expdiophlem2  38109  dvcosax  40662  ismgmhm  42311  2zrngamgm  42467  rnghmsscmap2  42501  rnghmsscmap  42502  funcrngcsetc  42526  rhmsscmap2  42547  rhmsscmap  42548  funcringcsetc  42563