Theorem oveqan12d 5963

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1373  (class class class)co 5944

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-rex 2490  df-v 2774  df-un 3170  df-sn 3639  df-pr 3640  df-op 3642  df-uni 3851  df-br 4045  df-iota 5232  df-fv 5279  df-ov 5947

This theorem is referenced by:  oveqan12rd  5964  offval  6166  offval3  6219  ecovdi  6733  ecovidi  6734  distrpig  7446  addcmpblnq  7480  addpipqqs  7483  mulpipq  7485  addcomnqg  7494  addcmpblnq0  7556  distrnq0  7572  recexprlem1ssl  7746  recexprlem1ssu  7747  1idsr  7881  addcnsrec  7955  mulcnsrec  7956  mulrid  8069  mulsub  8473  mulsub2  8474  muleqadd  8741  divmuldivap  8785  div2subap  8910  addltmul  9274  xnegdi  9990  fzsubel  10182  fzoval  10270  mulexp  10723  sqdivap  10748  crim  11169  readd  11180  remullem  11182  imadd  11188  cjadd  11195  cjreim  11214  sqrtmul  11346  sqabsadd  11366  sqabssub  11367  absmul  11380  abs2dif  11417  binom  11795  sinadd  12047  cosadd  12048  dvds2ln  12135  absmulgcd  12338  gcddiv  12340  bezoutr1  12354  lcmgcd  12400  nn0gcdsq  12522  crth  12546  pythagtriplem1  12588  pcqmul  12626  4sqlem4a  12714  4sqlem4  12715  prdsplusgval  13115  prdsmulrval  13117  idmhm  13301  resmhm  13319  eqgval  13559  idghm  13595  resghm  13596  isrhm  13920  rhmval  13935  xmetxp  14979  xmetxpbl  14980  txmetcnp  14990  divcnap  15037  rescncf  15053  relogoprlem  15340  lgsdir2  15510