Theorem oveqdr 7448

Description: Equality of two operations for any two operands. Useful in proofs using *propd theorems. (Contributed by Mario Carneiro, 29-Jun-2015.)

Hypothesis

Ref	Expression
oveqdr.1	⊢ (𝜑 → 𝐹 = 𝐺)

Assertion

Ref	Expression
oveqdr	⊢ ((𝜑 ∧ 𝜓) → (𝑥𝐹𝑦) = (𝑥𝐺𝑦))

Proof of Theorem oveqdr

Step	Hyp	Ref	Expression
1		oveqdr.1	. . 3 ⊢ (𝜑 → 𝐹 = 𝐺)
2	1	oveqd 7437	. 2 ⊢ (𝜑 → (𝑥𝐹𝑦) = (𝑥𝐺𝑦))
3	2	adantr 486	1 ⊢ ((𝜑 ∧ 𝜓) → (𝑥𝐹𝑦) = (𝑥𝐺𝑦))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569  (class class class)co 7420

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6546  df-ov 7423

This theorem is used by:  fullresc  18026  fucpropd  18155  resssetc  18267  resscatc  18284  issstrmgm  18831  gsumpropd  18867  issubmgm2  18892  grpsubpropd  19255  sylow2blem2  19835  isrngd  20395  prdsrngd  20398  isringd  20522  prdsringd  20550  prdscrngd  20551  prds1  20552  rnghmval  20670  pwsco1rhm  20741  pwsco2rhm  20742  pwsdiagrhm  20859  rnghmsubcsetclem1  20883  rnghmsubcsetclem2  20884  rngcifuestrc  20891  rhmsubcsetclem1  20912  rhmsubcsetclem2  20913  rhmsubcrngclem1  20918  rhmsubcrngclem2  20919  isdomn  20957  primefld  21062  sraring  21461  sralmod  21462  sralmod0  21463  issubrgd  21464  znzrh  21848  zncrng  21850  phlssphl  21965  opsrcrng  22368  opsrassa  22369  ply1lss  22514  ply1subrg  22515  opsr0  22536  opsr1  22537  subrgply1  22550  opsrring  22562  opsrlmod  22563  ply1mpl0  22574  ply1mpl1  22576  ply1ascl  22577  coe1tm  22592  evls1rhm  22640  evl1rhm  22650  evl1expd  22663  evls1maplmhm  22695  mat0  22732  matinvg  22733  matlmod  22744  scmatsrng1  22838  1mavmul  22863  mat2pmatmul  23049  ressprdsds  24690  nmpropd  24913  tng0  24962  tngngp2  24971  tnggrpr  24974  tngnrg  24993  sranlm  25003  pi1addval  25369  cvsi  25451  tcphphl  25548  abvpropd2  33526  resv0g  33899  resvcmn  33901  sra1r  34213  sradrng  34214  sraidom  34215  srasubrg  34216  srapwov  34221  drgextlsp  34226  tnglvec  34244  tngdim  34245  matdim  34247  fedgmullem2  34262  fldextrspunfld  34308  zhmnrg  34597  prdsbnd  38728  prdstotbnd  38729  prdsbnd2  38730  erngdvlem3  42048  erngdvlem3-rN  42056  hlhils0  43003  hlhils1N  43004  hlhillvec  43009  hlhildrng  43010  hlhil0  43013  hlhillsm  43014  zndvdchrrhm  43024  isprimroot  43144  primrootsunit1  43148  mendval  44181  mnring0gd  45219  mnringlmodd  45224  ovmpt4d  49975  upfval  50284  prcofvalg  50484