Theorem oveqan12d 6020

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1395  (class class class)co 6001

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-v 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-br 4084  df-iota 5278  df-fv 5326  df-ov 6004

This theorem is referenced by:  oveqan12rd  6021  offval  6226  offval3  6279  ecovdi  6793  ecovidi  6794  distrpig  7520  addcmpblnq  7554  addpipqqs  7557  mulpipq  7559  addcomnqg  7568  addcmpblnq0  7630  distrnq0  7646  recexprlem1ssl  7820  recexprlem1ssu  7821  1idsr  7955  addcnsrec  8029  mulcnsrec  8030  mulrid  8143  mulsub  8547  mulsub2  8548  muleqadd  8815  divmuldivap  8859  div2subap  8984  addltmul  9348  xnegdi  10064  fzsubel  10256  fzoval  10344  mulexp  10800  sqdivap  10825  crim  11369  readd  11380  remullem  11382  imadd  11388  cjadd  11395  cjreim  11414  sqrtmul  11546  sqabsadd  11566  sqabssub  11567  absmul  11580  abs2dif  11617  binom  11995  sinadd  12247  cosadd  12248  dvds2ln  12335  absmulgcd  12538  gcddiv  12540  bezoutr1  12554  lcmgcd  12600  nn0gcdsq  12722  crth  12746  pythagtriplem1  12788  pcqmul  12826  4sqlem4a  12914  4sqlem4  12915  prdsplusgval  13316  prdsmulrval  13318  idmhm  13502  resmhm  13520  eqgval  13760  idghm  13796  resghm  13797  isrhm  14122  rhmval  14137  xmetxp  15181  xmetxpbl  15182  txmetcnp  15192  divcnap  15239  rescncf  15255  relogoprlem  15542  lgsdir2  15712