Theorem oveqan12rd 7468

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537  (class class class)co 7448

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-ov 7451

This theorem is referenced by:  addpipq  11006  mulgt0sr  11174  mulcnsr  11205  mulresr  11208  recdiv  12000  revccat  14814  rlimdiv  15694  caucvg  15727  divgcdcoprm0  16712  estrchom  18195  funcestrcsetclem5  18213  ismgmhm  18734  ismhm  18820  rnghmsscmap2  20651  rnghmsscmap  20652  funcrngcsetc  20662  rhmsscmap2  20680  rhmsscmap  20681  funcringcsetc  20696  xrsdsval  21451  mpfrcl  22132  matval  22436  ucnval  24307  volcn  25660  dvres2lem  25965  dvid  25973  c1lip3  26058  taylthlem1  26433  abelthlem9  26502  2sqnn  27501  brbtwn2  28938  nonbooli  31683  0cnop  32011  0cnfn  32012  idcnop  32013  bccolsum  35701  ftc1anc  37661  rmydioph  42971  expdiophlem2  42979  dvcosax  45847  2zrngamgm  47968