Theorem oveqan12d 6047

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1398  (class class class)co 6028

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-rex 2517  df-v 2805  df-un 3205  df-sn 3679  df-pr 3680  df-op 3682  df-uni 3899  df-br 4094  df-iota 5293  df-fv 5341  df-ov 6031

This theorem is referenced by:  oveqan12rd  6048  offval  6252  offval3  6305  ecovdi  6858  ecovidi  6859  distrpig  7613  addcmpblnq  7647  addpipqqs  7650  mulpipq  7652  addcomnqg  7661  addcmpblnq0  7723  distrnq0  7739  recexprlem1ssl  7913  recexprlem1ssu  7914  1idsr  8048  addcnsrec  8122  mulcnsrec  8123  mulrid  8236  mulsub  8639  mulsub2  8640  muleqadd  8907  divmuldivap  8951  div2subap  9076  addltmul  9440  xnegdi  10164  fzsubel  10357  fzoval  10445  mulexp  10903  sqdivap  10928  crim  11498  readd  11509  remullem  11511  imadd  11517  cjadd  11524  cjreim  11543  sqrtmul  11675  sqabsadd  11695  sqabssub  11696  absmul  11709  abs2dif  11746  binom  12125  sinadd  12377  cosadd  12378  dvds2ln  12465  absmulgcd  12668  gcddiv  12670  bezoutr1  12684  lcmgcd  12730  nn0gcdsq  12852  crth  12876  pythagtriplem1  12918  pcqmul  12956  4sqlem4a  13044  4sqlem4  13045  prdsplusgval  13446  prdsmulrval  13448  idmhm  13632  resmhm  13650  eqgval  13890  idghm  13926  resghm  13927  isrhm  14253  rhmval  14268  xmetxp  15318  xmetxpbl  15319  txmetcnp  15329  divcnap  15376  rescncf  15392  relogoprlem  15679  lgsdir2  15852  clwwlknccat  16364