Theorem oveqan12d 5884

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1353  (class class class)co 5865

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 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-rex 2459  df-v 2737  df-un 3131  df-sn 3595  df-pr 3596  df-op 3598  df-uni 3806  df-br 3999  df-iota 5170  df-fv 5216  df-ov 5868

This theorem is referenced by:  oveqan12rd  5885  offval  6080  offval3  6125  ecovdi  6636  ecovidi  6637  distrpig  7307  addcmpblnq  7341  addpipqqs  7344  mulpipq  7346  addcomnqg  7355  addcmpblnq0  7417  distrnq0  7433  recexprlem1ssl  7607  recexprlem1ssu  7608  1idsr  7742  addcnsrec  7816  mulcnsrec  7817  mulid1  7929  mulsub  8332  mulsub2  8333  muleqadd  8598  divmuldivap  8642  div2subap  8767  addltmul  9128  xnegdi  9839  fzsubel  10030  fzoval  10118  mulexp  10529  sqdivap  10554  crim  10835  readd  10846  remullem  10848  imadd  10854  cjadd  10861  cjreim  10880  sqrtmul  11012  sqabsadd  11032  sqabssub  11033  absmul  11046  abs2dif  11083  binom  11460  sinadd  11712  cosadd  11713  dvds2ln  11799  absmulgcd  11985  gcddiv  11987  bezoutr1  12001  lcmgcd  12045  nn0gcdsq  12167  crth  12191  pythagtriplem1  12232  pcqmul  12270  4sqlem4a  12356  4sqlem4  12357  idmhm  12723  xmetxp  13578  xmetxpbl  13579  txmetcnp  13589  divcnap  13626  rescncf  13639  relogoprlem  13860  lgsdir2  14005