Theorem oveqan12rd 7178

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

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1537  (class class class)co 7158

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-iota 6316  df-fv 6365  df-ov 7161

This theorem is referenced by:  addpipq  10361  mulgt0sr  10529  mulcnsr  10560  mulresr  10563  recdiv  11348  revccat  14130  rlimdiv  15004  caucvg  15037  divgcdcoprm0  16011  estrchom  17379  funcestrcsetclem5  17396  ismhm  17960  mpfrcl  20300  xrsdsval  20591  matval  21022  ucnval  22888  volcn  24209  dvres2lem  24510  dvid  24517  c1lip3  24598  taylthlem1  24963  abelthlem9  25030  2sqnn  26017  brbtwn2  26693  nonbooli  29430  0cnop  29758  0cnfn  29759  idcnop  29760  bccolsum  32973  ftc1anc  34977  rmydioph  39618  expdiophlem2  39626  dvcosax  42218  ismgmhm  44057  2zrngamgm  44217  rnghmsscmap2  44251  rnghmsscmap  44252  funcrngcsetc  44276  rhmsscmap2  44297  rhmsscmap  44298  funcringcsetc  44313