Theorem oveqdr 7458

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1536  (class class class)co 7430

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-ss 3979  df-uni 4912  df-br 5148  df-iota 6515  df-fv 6570  df-ov 7433

This theorem is referenced by:  fullresc  17901  fucpropd  18033  resssetc  18145  resscatc  18162  issstrmgm  18678  gsumpropd  18703  issubmgm2  18728  grpsubpropd  19075  sylow2blem2  19653  isrngd  20190  prdsrngd  20193  isringd  20304  prdsringd  20334  prdscrngd  20335  prds1  20336  rnghmval  20456  pwsco1rhm  20518  pwsco2rhm  20519  pwsdiagrhm  20623  rnghmsubcsetclem1  20647  rnghmsubcsetclem2  20648  rngcifuestrc  20655  rhmsubcsetclem1  20676  rhmsubcsetclem2  20677  rhmsubcrngclem1  20682  rhmsubcrngclem2  20683  isdomn  20721  primefld  20822  sraring  21210  sralmod  21211  sralmod0  21212  issubrgd  21213  znzrh  21578  zncrng  21580  phlssphl  21694  sraassaOLD  21907  opsrcrng  22100  opsrassa  22101  ply1lss  22213  ply1subrg  22214  opsr0  22235  opsr1  22236  subrgply1  22249  opsrring  22261  opsrlmod  22262  ply1mpl0  22273  ply1mpl1  22275  ply1ascl  22276  coe1tm  22291  evls1rhm  22341  evl1rhm  22351  evl1expd  22364  evls1maplmhm  22396  mat0  22438  matinvg  22439  matlmod  22450  scmatsrng1  22544  1mavmul  22569  mat2pmatmul  22752  ressprdsds  24396  nmpropd  24622  tng0  24674  tngngp2  24688  tnggrpr  24691  tngnrg  24710  sranlm  24720  pi1addval  25094  cvsi  25176  tcphphl  25274  abvpropd2  32934  resv0g  33346  resvcmn  33348  sra1r  33611  sradrng  33612  srasubrg  33613  drgextlsp  33622  tnglvec  33639  tngdim  33640  matdim  33642  fedgmullem2  33657  zhmnrg  33927  prdsbnd  37779  prdstotbnd  37780  prdsbnd2  37781  erngdvlem3  40972  erngdvlem3-rN  40980  hlhils0  41931  hlhils1N  41932  hlhillvec  41937  hlhildrng  41938  hlhil0  41941  hlhillsm  41942  zndvdchrrhm  41952  isprimroot  42074  primrootsunit1  42078  mendval  43167  mnring0gd  44214  mnringlmodd  44221