Theorem oveqdr 7377

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

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-ss 3920  df-uni 4859  df-br 5093  df-iota 6438  df-fv 6490  df-ov 7352

This theorem is referenced by:  fullresc  17758  fucpropd  17887  resssetc  17999  resscatc  18016  issstrmgm  18527  gsumpropd  18552  issubmgm2  18577  grpsubpropd  18924  sylow2blem2  19500  isrngd  20058  prdsrngd  20061  isringd  20176  prdsringd  20206  prdscrngd  20207  prds1  20208  rnghmval  20325  pwsco1rhm  20387  pwsco2rhm  20388  pwsdiagrhm  20492  rnghmsubcsetclem1  20516  rnghmsubcsetclem2  20517  rngcifuestrc  20524  rhmsubcsetclem1  20545  rhmsubcsetclem2  20546  rhmsubcrngclem1  20551  rhmsubcrngclem2  20552  isdomn  20590  primefld  20690  sraring  21090  sralmod  21091  sralmod0  21092  issubrgd  21093  znzrh  21449  zncrng  21451  phlssphl  21566  sraassaOLD  21777  opsrcrng  21964  opsrassa  21965  ply1lss  22079  ply1subrg  22080  opsr0  22101  opsr1  22102  subrgply1  22115  opsrring  22127  opsrlmod  22128  ply1mpl0  22139  ply1mpl1  22141  ply1ascl  22142  coe1tm  22157  evls1rhm  22207  evl1rhm  22217  evl1expd  22230  evls1maplmhm  22262  mat0  22302  matinvg  22303  matlmod  22314  scmatsrng1  22408  1mavmul  22433  mat2pmatmul  22616  ressprdsds  24257  nmpropd  24480  tng0  24529  tngngp2  24538  tnggrpr  24541  tngnrg  24560  sranlm  24570  pi1addval  24946  cvsi  25028  tcphphl  25125  abvpropd2  32916  resv0g  33285  resvcmn  33287  sra1r  33563  sradrng  33564  sraidom  33565  srasubrg  33566  srapwov  33571  drgextlsp  33576  tnglvec  33595  tngdim  33596  matdim  33598  fedgmullem2  33613  fldextrspunfld  33659  zhmnrg  33948  prdsbnd  37793  prdstotbnd  37794  prdsbnd2  37795  erngdvlem3  40989  erngdvlem3-rN  40997  hlhils0  41944  hlhils1N  41945  hlhillvec  41950  hlhildrng  41951  hlhil0  41954  hlhillsm  41955  zndvdchrrhm  41965  isprimroot  42086  primrootsunit1  42090  mendval  43172  mnring0gd  44214  mnringlmodd  44219  ovmpt4d  48869  upfval  49181  prcofvalg  49381