Theorem oveqan12d 5915

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1364  (class class class)co 5896

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-rex 2474  df-v 2754  df-un 3148  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-br 4019  df-iota 5196  df-fv 5243  df-ov 5899

This theorem is referenced by:  oveqan12rd  5916  offval  6114  offval3  6159  ecovdi  6672  ecovidi  6673  distrpig  7362  addcmpblnq  7396  addpipqqs  7399  mulpipq  7401  addcomnqg  7410  addcmpblnq0  7472  distrnq0  7488  recexprlem1ssl  7662  recexprlem1ssu  7663  1idsr  7797  addcnsrec  7871  mulcnsrec  7872  mulrid  7984  mulsub  8388  mulsub2  8389  muleqadd  8655  divmuldivap  8699  div2subap  8824  addltmul  9185  xnegdi  9898  fzsubel  10090  fzoval  10178  mulexp  10590  sqdivap  10615  crim  10899  readd  10910  remullem  10912  imadd  10918  cjadd  10925  cjreim  10944  sqrtmul  11076  sqabsadd  11096  sqabssub  11097  absmul  11110  abs2dif  11147  binom  11524  sinadd  11776  cosadd  11777  dvds2ln  11863  absmulgcd  12050  gcddiv  12052  bezoutr1  12066  lcmgcd  12110  nn0gcdsq  12232  crth  12256  pythagtriplem1  12297  pcqmul  12335  4sqlem4a  12423  4sqlem4  12424  idmhm  12921  resmhm  12939  eqgval  13162  idghm  13198  resghm  13199  isrhm  13508  rhmval  13523  xmetxp  14467  xmetxpbl  14468  txmetcnp  14478  divcnap  14515  rescncf  14528  relogoprlem  14749  lgsdir2  14895