Theorem oveqdr 7409

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

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1550  (class class class)co 7381

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-ext 2724

This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1553  df-ex 1790  df-sb 2081  df-clab 2731  df-cleq 2744  df-clel 2827  df-v 3446  df-ss 3912  df-uni 4856  df-br 5091  df-iota 6462  df-fv 6514  df-ov 7384

This theorem is referenced by:  fullresc  17856  fucpropd  17985  resssetc  18097  resscatc  18114  issstrmgm  18659  gsumpropd  18684  issubmgm2  18709  grpsubpropd  19059  sylow2blem2  19633  isrngd  20191  prdsrngd  20194  isringd  20309  prdsringd  20337  prdscrngd  20338  prds1  20339  rnghmval  20457  pwsco1rhm  20519  pwsco2rhm  20520  pwsdiagrhm  20625  rnghmsubcsetclem1  20649  rnghmsubcsetclem2  20650  rngcifuestrc  20657  rhmsubcsetclem1  20678  rhmsubcsetclem2  20679  rhmsubcrngclem1  20684  rhmsubcrngclem2  20685  isdomn  20723  primefld  20823  sraring  21222  sralmod  21223  sralmod0  21224  issubrgd  21225  znzrh  21563  zncrng  21565  phlssphl  21680  opsrcrng  22081  opsrassa  22082  ply1lss  22227  ply1subrg  22228  opsr0  22249  opsr1  22250  subrgply1  22263  opsrring  22275  opsrlmod  22276  ply1mpl0  22287  ply1mpl1  22289  ply1ascl  22290  coe1tm  22305  evls1rhm  22354  evl1rhm  22364  evl1expd  22377  evls1maplmhm  22409  mat0  22446  matinvg  22447  matlmod  22458  scmatsrng1  22552  1mavmul  22577  mat2pmatmul  22760  ressprdsds  24400  nmpropd  24623  tng0  24672  tngngp2  24681  tnggrpr  24684  tngnrg  24703  sranlm  24713  pi1addval  25079  cvsi  25161  tcphphl  25258  abvpropd2  33093  resv0g  33470  resvcmn  33472  sra1r  33822  sradrng  33823  sraidom  33824  srasubrg  33825  srapwov  33830  drgextlsp  33835  tnglvec  33853  tngdim  33854  matdim  33856  fedgmullem2  33871  fldextrspunfld  33917  zhmnrg  34206  prdsbnd  38230  prdstotbnd  38231  prdsbnd2  38232  erngdvlem3  41552  erngdvlem3-rN  41560  hlhils0  42507  hlhils1N  42508  hlhillvec  42513  hlhildrng  42514  hlhil0  42517  hlhillsm  42518  zndvdchrrhm  42528  isprimroot  42648  primrootsunit1  42652  mendval  43694  mnring0gd  44735  mnringlmodd  44740  ovmpt4d  49424  upfval  49735  prcofvalg  49935