Theorem oveqdr 7459

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 7448	. 2 ⊢ (𝜑 → (𝑥𝐹𝑦) = (𝑥𝐺𝑦))
3	2	adantr 480	1 ⊢ ((𝜑 ∧ 𝜓) → (𝑥𝐹𝑦) = (𝑥𝐺𝑦))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540  (class class class)co 7431

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-ss 3968  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-ov 7434

This theorem is referenced by:  fullresc  17896  fucpropd  18025  resssetc  18137  resscatc  18154  issstrmgm  18666  gsumpropd  18691  issubmgm2  18716  grpsubpropd  19063  sylow2blem2  19639  isrngd  20170  prdsrngd  20173  isringd  20288  prdsringd  20318  prdscrngd  20319  prds1  20320  rnghmval  20440  pwsco1rhm  20502  pwsco2rhm  20503  pwsdiagrhm  20607  rnghmsubcsetclem1  20631  rnghmsubcsetclem2  20632  rngcifuestrc  20639  rhmsubcsetclem1  20660  rhmsubcsetclem2  20661  rhmsubcrngclem1  20666  rhmsubcrngclem2  20667  isdomn  20705  primefld  20806  sraring  21193  sralmod  21194  sralmod0  21195  issubrgd  21196  znzrh  21561  zncrng  21563  phlssphl  21677  sraassaOLD  21890  opsrcrng  22083  opsrassa  22084  ply1lss  22198  ply1subrg  22199  opsr0  22220  opsr1  22221  subrgply1  22234  opsrring  22246  opsrlmod  22247  ply1mpl0  22258  ply1mpl1  22260  ply1ascl  22261  coe1tm  22276  evls1rhm  22326  evl1rhm  22336  evl1expd  22349  evls1maplmhm  22381  mat0  22423  matinvg  22424  matlmod  22435  scmatsrng1  22529  1mavmul  22554  mat2pmatmul  22737  ressprdsds  24381  nmpropd  24607  tng0  24659  tngngp2  24673  tnggrpr  24676  tngnrg  24695  sranlm  24705  pi1addval  25081  cvsi  25163  tcphphl  25261  abvpropd2  32950  resv0g  33367  resvcmn  33369  sra1r  33632  sradrng  33633  sraidom  33634  srasubrg  33635  drgextlsp  33644  tnglvec  33663  tngdim  33664  matdim  33666  fedgmullem2  33681  fldextrspunfld  33726  zhmnrg  33966  prdsbnd  37800  prdstotbnd  37801  prdsbnd2  37802  erngdvlem3  40992  erngdvlem3-rN  41000  hlhils0  41951  hlhils1N  41952  hlhillvec  41957  hlhildrng  41958  hlhil0  41961  hlhillsm  41962  zndvdchrrhm  41972  isprimroot  42094  primrootsunit1  42098  mendval  43191  mnring0gd  44238  mnringlmodd  44245  ovmpt4d  48768  upfval  48933