Theorem oveqdr 7397

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

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

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 3446  df-ss 3928  df-uni 4868  df-br 5103  df-iota 6452  df-fv 6507  df-ov 7372

This theorem is referenced by:  fullresc  17793  fucpropd  17922  resssetc  18034  resscatc  18051  issstrmgm  18562  gsumpropd  18587  issubmgm2  18612  grpsubpropd  18959  sylow2blem2  19535  isrngd  20093  prdsrngd  20096  isringd  20211  prdsringd  20241  prdscrngd  20242  prds1  20243  rnghmval  20360  pwsco1rhm  20422  pwsco2rhm  20423  pwsdiagrhm  20527  rnghmsubcsetclem1  20551  rnghmsubcsetclem2  20552  rngcifuestrc  20559  rhmsubcsetclem1  20580  rhmsubcsetclem2  20581  rhmsubcrngclem1  20586  rhmsubcrngclem2  20587  isdomn  20625  primefld  20725  sraring  21125  sralmod  21126  sralmod0  21127  issubrgd  21128  znzrh  21484  zncrng  21486  phlssphl  21601  sraassaOLD  21812  opsrcrng  21999  opsrassa  22000  ply1lss  22114  ply1subrg  22115  opsr0  22136  opsr1  22137  subrgply1  22150  opsrring  22162  opsrlmod  22163  ply1mpl0  22174  ply1mpl1  22176  ply1ascl  22177  coe1tm  22192  evls1rhm  22242  evl1rhm  22252  evl1expd  22265  evls1maplmhm  22297  mat0  22337  matinvg  22338  matlmod  22349  scmatsrng1  22443  1mavmul  22468  mat2pmatmul  22651  ressprdsds  24292  nmpropd  24515  tng0  24564  tngngp2  24573  tnggrpr  24576  tngnrg  24595  sranlm  24605  pi1addval  24981  cvsi  25063  tcphphl  25160  abvpropd2  32937  resv0g  33303  resvcmn  33305  sra1r  33570  sradrng  33571  sraidom  33572  srasubrg  33573  drgextlsp  33582  tnglvec  33601  tngdim  33602  matdim  33604  fedgmullem2  33619  fldextrspunfld  33664  zhmnrg  33948  prdsbnd  37780  prdstotbnd  37781  prdsbnd2  37782  erngdvlem3  40977  erngdvlem3-rN  40985  hlhils0  41932  hlhils1N  41933  hlhillvec  41938  hlhildrng  41939  hlhil0  41942  hlhillsm  41943  zndvdchrrhm  41953  isprimroot  42074  primrootsunit1  42078  mendval  43161  mnring0gd  44203  mnringlmodd  44208  ovmpt4d  48846  upfval  49158  prcofvalg  49358