Theorem oveqan12d 6036

Description: Equality deduction for operation value. (Contributed by NM, 10-Aug-1995.)

Hypotheses

Ref	Expression
oveq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)
opreqan12i.2	⊢ (𝜓 → 𝐶 = 𝐷)

Assertion

Ref	Expression
oveqan12d	⊢ ((𝜑 ∧ 𝜓) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))

Proof of Theorem oveqan12d

Step	Hyp	Ref	Expression
1		oveq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		opreqan12i.2	. 2 ⊢ (𝜓 → 𝐶 = 𝐷)
3		oveq12 6026	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
4	1, 2, 3	syl2an 289	1 ⊢ ((𝜑 ∧ 𝜓) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1397  (class class class)co 6017

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rex 2516  df-v 2804  df-un 3204  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-iota 5286  df-fv 5334  df-ov 6020

This theorem is referenced by:  oveqan12rd  6037  offval  6242  offval3  6295  ecovdi  6814  ecovidi  6815  distrpig  7552  addcmpblnq  7586  addpipqqs  7589  mulpipq  7591  addcomnqg  7600  addcmpblnq0  7662  distrnq0  7678  recexprlem1ssl  7852  recexprlem1ssu  7853  1idsr  7987  addcnsrec  8061  mulcnsrec  8062  mulrid  8175  mulsub  8579  mulsub2  8580  muleqadd  8847  divmuldivap  8891  div2subap  9016  addltmul  9380  xnegdi  10102  fzsubel  10294  fzoval  10382  mulexp  10839  sqdivap  10864  crim  11418  readd  11429  remullem  11431  imadd  11437  cjadd  11444  cjreim  11463  sqrtmul  11595  sqabsadd  11615  sqabssub  11616  absmul  11629  abs2dif  11666  binom  12044  sinadd  12296  cosadd  12297  dvds2ln  12384  absmulgcd  12587  gcddiv  12589  bezoutr1  12603  lcmgcd  12649  nn0gcdsq  12771  crth  12795  pythagtriplem1  12837  pcqmul  12875  4sqlem4a  12963  4sqlem4  12964  prdsplusgval  13365  prdsmulrval  13367  idmhm  13551  resmhm  13569  eqgval  13809  idghm  13845  resghm  13846  isrhm  14171  rhmval  14186  xmetxp  15230  xmetxpbl  15231  txmetcnp  15241  divcnap  15288  rescncf  15304  relogoprlem  15591  lgsdir2  15761  clwwlknccat  16273