Theorem oveqdr 6103

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1402  (class class class)co 6075

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-uni 3931  df-br 4126  df-iota 5332  df-fv 5380  df-ov 6078

This theorem is referenced by:  grppropstrg  13801  grpsubpropdg  13886  isrngd  14227  crngpropd  14317  isringd  14319  ring1  14337  opprrng  14355  opprrngbg  14356  opprring  14357  opprringbg  14358  opprsubgg  14363  mulgass3  14364  rngidpropdg  14426  invrpropdg  14429  subrngpropd  14497  subrgpropd  14534  isdomn  14551  aprprop  14574  sraring  14758  sralmod  14759  sralmod0g  14760  issubrgd  14761  rlmvnegg  14774  lidlrsppropdg  14804  crngridl  14839  znzrh  14950  zncrng  14952