Theorem oveqdr 6932

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

Syntax hints:   → wi 4   ∧ wa 386   = wceq 1658  (class class class)co 6904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-ext 2802

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2811  df-cleq 2817  df-clel 2820  df-nfc 2957  df-rex 3122  df-uni 4658  df-br 4873  df-iota 6085  df-fv 6130  df-ov 6907

This theorem is referenced by:  fullresc  16862  fucpropd  16988  resssetc  17093  resscatc  17106  issstrmgm  17604  gsumpropd  17624  grpsubpropd  17873  sylow2blem2  18386  isringd  18938  prdsringd  18965  prdscrngd  18966  prds1  18967  pwsco1rhm  19093  pwsco2rhm  19094  pwsdiagrhm  19168  sralmod  19547  sralmod0  19548  issubrngd2  19549  isdomn  19654  sraassa  19685  opsrcrng  19847  opsrassa  19848  ply1lss  19925  ply1subrg  19926  opsr0  19947  opsr1  19948  subrgply1  19962  opsrring  19974  opsrlmod  19975  ply1mpl0  19984  ply1mpl1  19986  ply1ascl  19987  coe1tm  20002  evls1rhm  20046  evl1rhm  20055  evl1expd  20068  znzrh  20249  zncrng  20251  phlssphl  20365  mat0  20589  matinvg  20590  matlmod  20601  scmatsrng1  20696  1mavmul  20721  mat2pmatmul  20905  ressprdsds  22545  nmpropd  22767  tng0  22816  tngngp2  22825  tnggrpr  22828  tngnrg  22847  sranlm  22857  tcphphl  23394  istrkgc  25765  istrkgb  25766  abvpropd2  30196  resv0g  30380  resvcmn  30382  zhmnrg  30555  prdsbnd  34133  prdstotbnd  34134  prdsbnd2  34135  erngdvlem3  37064  erngdvlem3-rN  37072  hlhils0  38019  hlhils1N  38020  hlhillvec  38025  hlhildrng  38026  hlhil0  38029  hlhillsm  38030  mendval  38595  issubmgm2  42636  rnghmval  42737  lidlmmgm  42771  rnghmsubcsetclem1  42821  rnghmsubcsetclem2  42822  rngcifuestrc  42843  rhmsubcsetclem1  42867  rhmsubcsetclem2  42868  rhmsubcrngclem1  42873  rhmsubcrngclem2  42874