Theorem oveqan12d 5894

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

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

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 2740  df-un 3134  df-sn 3599  df-pr 3600  df-op 3602  df-uni 3811  df-br 4005  df-iota 5179  df-fv 5225  df-ov 5878

This theorem is referenced by:  oveqan12rd  5895  offval  6090  offval3  6135  ecovdi  6646  ecovidi  6647  distrpig  7332  addcmpblnq  7366  addpipqqs  7369  mulpipq  7371  addcomnqg  7380  addcmpblnq0  7442  distrnq0  7458  recexprlem1ssl  7632  recexprlem1ssu  7633  1idsr  7767  addcnsrec  7841  mulcnsrec  7842  mulrid  7954  mulsub  8358  mulsub2  8359  muleqadd  8625  divmuldivap  8669  div2subap  8794  addltmul  9155  xnegdi  9868  fzsubel  10060  fzoval  10148  mulexp  10559  sqdivap  10584  crim  10867  readd  10878  remullem  10880  imadd  10886  cjadd  10893  cjreim  10912  sqrtmul  11044  sqabsadd  11064  sqabssub  11065  absmul  11078  abs2dif  11115  binom  11492  sinadd  11744  cosadd  11745  dvds2ln  11831  absmulgcd  12018  gcddiv  12020  bezoutr1  12034  lcmgcd  12078  nn0gcdsq  12200  crth  12224  pythagtriplem1  12265  pcqmul  12303  4sqlem4a  12389  4sqlem4  12390  idmhm  12860  eqgval  13082  xmetxp  14010  xmetxpbl  14011  txmetcnp  14021  divcnap  14058  rescncf  14071  relogoprlem  14292  lgsdir2  14437