Theorem oveqan12d 5896

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

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

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-v 2741  df-un 3135  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-br 4006  df-iota 5180  df-fv 5226  df-ov 5880

This theorem is referenced by:  oveqan12rd  5897  offval  6092  offval3  6137  ecovdi  6648  ecovidi  6649  distrpig  7334  addcmpblnq  7368  addpipqqs  7371  mulpipq  7373  addcomnqg  7382  addcmpblnq0  7444  distrnq0  7460  recexprlem1ssl  7634  recexprlem1ssu  7635  1idsr  7769  addcnsrec  7843  mulcnsrec  7844  mulrid  7956  mulsub  8360  mulsub2  8361  muleqadd  8627  divmuldivap  8671  div2subap  8796  addltmul  9157  xnegdi  9870  fzsubel  10062  fzoval  10150  mulexp  10561  sqdivap  10586  crim  10869  readd  10880  remullem  10882  imadd  10888  cjadd  10895  cjreim  10914  sqrtmul  11046  sqabsadd  11066  sqabssub  11067  absmul  11080  abs2dif  11117  binom  11494  sinadd  11746  cosadd  11747  dvds2ln  11833  absmulgcd  12020  gcddiv  12022  bezoutr1  12036  lcmgcd  12080  nn0gcdsq  12202  crth  12226  pythagtriplem1  12267  pcqmul  12305  4sqlem4a  12391  4sqlem4  12392  idmhm  12865  eqgval  13087  xmetxp  14092  xmetxpbl  14093  txmetcnp  14103  divcnap  14140  rescncf  14153  relogoprlem  14374  lgsdir2  14519