Theorem oveqan12d 7445

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

Syntax hints:   → wi 4   ∧ wa 394   = wceq 1534  (class class class)co 7426

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-rab 3420  df-v 3464  df-dif 3950  df-un 3952  df-ss 3964  df-nul 4326  df-if 4534  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4916  df-br 5156  df-iota 6508  df-fv 6564  df-ov 7429

This theorem is referenced by:  oveqan12rd  7446  offval  7701  offval3  7998  odi  8611  omopth2  8616  oeoa  8629  ecovdi  8856  ackbij1lem9  10273  distrpi  10943  addpipq  10982  mulpipq  10985  lterpq  11015  reclem3pr  11094  1idsr  11143  mulcnsr  11181  mulrid  11264  1re  11266  mul02  11444  addcom  11452  mulsub  11709  mulsub2  11710  muleqadd  11910  divmuldiv  11967  div2sub  12092  addltmul  12502  xnegdi  13283  xadddilem  13329  fzsubel  13593  fzoval  13689  seqid3  14068  mulexp  14123  sqdiv  14142  hashdom  14398  hashun  14401  ccatfval  14583  splcl  14762  crim  15122  readd  15133  remullem  15135  imadd  15141  cjadd  15148  cjreim  15167  sqrtmul  15266  sqabsadd  15289  sqabssub  15290  absmul  15301  abs2dif  15339  bhmafibid1  15472  binom  15836  binomfallfac  16045  sinadd  16168  cosadd  16169  dvds2ln  16293  sadcaddlem  16459  bezoutlem4  16545  bezout  16546  absmulgcd  16552  gcddiv  16554  bezoutr1  16572  lcmgcd  16610  lcmfass  16649  nn0gcdsq  16756  crth  16782  pythagtriplem1  16820  pcqmul  16857  4sqlem4a  16955  4sqlem4  16956  prdsplusgval  17490  prdsmulrval  17492  prdsdsval  17495  prdsvscaval  17496  idmgmhm  18696  resmgmhm  18706  idmhm  18787  0mhm  18811  resmhm  18812  prdspjmhm  18821  pwsdiagmhm  18823  gsumws2  18834  frmdup1  18856  eqgval  19173  idghm  19227  resghm  19228  mulgmhm  19827  mulgghm  19828  srglmhm  20206  srgrmhm  20207  ringlghm  20293  ringrghm  20294  gsumdixp  20300  isrhm  20462  rhmval  20484  issrngd  20836  lmodvsghm  20901  pwssplit2  21040  xrsdsval  21409  expmhm  21435  expghm  21467  mulgghm2  21468  mulgrhm  21469  pzriprnglem4  21476  cygznlem3  21569  asclghm  21882  psrmulfval  21954  evlslem4  22091  mpfrcl  22102  mamuval  22387  mamufv  22388  mvmulval  22539  mndifsplit  22632  mat2pmatmul  22727  decpmatmul  22768  fmval  23941  fmf  23943  flffval  23987  divcnOLD  24878  divcn  24880  rescncf  24911  htpyco1  24998  tcphcph  25259  rrxdsfival  25435  ehl2eudisval  25445  volun  25568  dyadval  25615  dvlip  26020  ftc1a  26066  ftc2ditglem  26074  tdeglem3  26087  tdeglem3OLD  26088  q1pval  26185  reefgim  26483  relogoprlem  26621  eflogeq  26632  zetacvg  27046  lgsdir2  27362  lgsdchr  27387  2sq2  27465  2sqnn0  27470  negsdi  28062  brbtwn2  28842  ax5seglem4  28869  axeuclid  28900  axcontlem2  28902  axcontlem4  28904  axcontlem8  28908  clwwlknccat  29999  ex-fpar  30398  ipasslem11  30776  hhssnv  31200  mayete3i  31664  idunop  31914  idhmop  31918  0lnfn  31921  lnopmi  31936  lnophsi  31937  lnopcoi  31939  hmops  31956  hmopm  31957  nlelshi  31996  cnlnadjlem2  32004  kbass6  32057  strlem3a  32188  hstrlem3a  32196  mndpluscn  33743  xrge0iifhom  33754  rezh  33788  probdsb  34258  resconn  35076  iscvm  35089  satfdmlem  35198  satffunlem1lem1  35232  satffunlem2lem1  35234  fwddifnval  35989  bj-bary1  37021  poimirlem15  37338  mbfposadd  37370  ftc1anclem3  37398  rrnmval  37531  dvhopaddN  40815  nnadddir  41989  cnreeu  42161  prjcrvfval  42301  pellex  42510  rmxfval  42579  rmyfval  42580  qirropth  42583  rmxycomplete  42593  jm2.15nn0  42679  rmxdioph  42692  expdiophlem2  42698  mendvsca  42870  deg1mhm  42883  mnringmulrvald  43919  addrval  44158  subrval  44159  fmulcl  45220  fmuldfeqlem1  45221  line  48138  itsclc0xyqsolr  48175