Theorem oveqan12d 6037

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 6027	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
4	1, 2, 3	syl2an 289	1 ⊢ ((𝜑 ∧ 𝜓) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))

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

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 6021

This theorem is referenced by:  oveqan12rd  6038  offval  6243  offval3  6296  ecovdi  6815  ecovidi  6816  distrpig  7553  addcmpblnq  7587  addpipqqs  7590  mulpipq  7592  addcomnqg  7601  addcmpblnq0  7663  distrnq0  7679  recexprlem1ssl  7853  recexprlem1ssu  7854  1idsr  7988  addcnsrec  8062  mulcnsrec  8063  mulrid  8176  mulsub  8580  mulsub2  8581  muleqadd  8848  divmuldivap  8892  div2subap  9017  addltmul  9381  xnegdi  10103  fzsubel  10295  fzoval  10383  mulexp  10841  sqdivap  10866  crim  11436  readd  11447  remullem  11449  imadd  11455  cjadd  11462  cjreim  11481  sqrtmul  11613  sqabsadd  11633  sqabssub  11634  absmul  11647  abs2dif  11684  binom  12063  sinadd  12315  cosadd  12316  dvds2ln  12403  absmulgcd  12606  gcddiv  12608  bezoutr1  12622  lcmgcd  12668  nn0gcdsq  12790  crth  12814  pythagtriplem1  12856  pcqmul  12894  4sqlem4a  12982  4sqlem4  12983  prdsplusgval  13384  prdsmulrval  13386  idmhm  13570  resmhm  13588  eqgval  13828  idghm  13864  resghm  13865  isrhm  14191  rhmval  14206  xmetxp  15250  xmetxpbl  15251  txmetcnp  15261  divcnap  15308  rescncf  15324  relogoprlem  15611  lgsdir2  15781  clwwlknccat  16293