MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  oveqan12rd Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 oveq1d.1 . . 3 (𝜑𝐴 = 𝐵)
2 opreqan12i.2 . . 3 (𝜓𝐶 = 𝐷)
31, 2oveqan12d 6833 . 2 ((𝜑𝜓) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
43ancoms 468 1 ((𝜓𝜑) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator