Theorem oveqan12d 7388

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540  (class class class)co 7369

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-iota 6452  df-fv 6507  df-ov 7372

This theorem is referenced by:  oveqan12rd  7389  offval  7642  offval3  7940  odi  8520  omopth2  8525  oeoa  8538  ecovdi  8775  ackbij1lem9  10156  distrpi  10827  addpipq  10866  mulpipq  10869  lterpq  10899  reclem3pr  10978  1idsr  11027  mulcnsr  11065  mulrid  11148  1re  11150  mul02  11328  addcom  11336  mulsub  11597  mulsub2  11598  muleqadd  11798  divmuldiv  11858  div2sub  11983  addltmul  12394  xnegdi  13184  xadddilem  13230  fzsubel  13497  fzoval  13597  seqid3  13987  mulexp  14042  sqdiv  14062  hashdom  14320  hashun  14323  ccatfval  14514  splcl  14693  crim  15057  readd  15068  remullem  15070  imadd  15076  cjadd  15083  cjreim  15102  sqrtmul  15201  sqabsadd  15224  sqabssub  15225  absmul  15236  abs2dif  15275  bhmafibid1  15410  binom  15772  binomfallfac  15983  sinadd  16108  cosadd  16109  dvds2ln  16235  sadcaddlem  16403  bezoutlem4  16488  bezout  16489  absmulgcd  16495  gcddiv  16497  bezoutr1  16515  lcmgcd  16553  lcmfass  16592  nn0gcdsq  16698  crth  16724  pythagtriplem1  16763  pcqmul  16800  4sqlem4a  16898  4sqlem4  16899  prdsplusgval  17412  prdsmulrval  17414  prdsdsval  17417  prdsvscaval  17418  idmgmhm  18610  resmgmhm  18620  idmhm  18704  0mhm  18728  resmhm  18729  prdspjmhm  18738  pwsdiagmhm  18740  gsumws2  18751  frmdup1  18773  eqgval  19091  idghm  19145  resghm  19146  mulgmhm  19741  mulgghm  19742  srglmhm  20141  srgrmhm  20142  ringlghm  20232  ringrghm  20233  gsumdixp  20239  isrhm  20398  rhmval  20420  issrngd  20775  lmodvsghm  20861  pwssplit2  20999  xrsdsval  21352  expmhm  21378  expghm  21417  mulgghm2  21418  mulgrhm  21419  pzriprnglem4  21426  cygznlem3  21511  asclghm  21825  psrmulfval  21885  evlslem4  22016  mpfrcl  22025  mamuval  22313  mamufv  22314  mvmulval  22463  mndifsplit  22556  mat2pmatmul  22651  decpmatmul  22692  fmval  23863  fmf  23865  flffval  23909  divcnOLD  24790  divcn  24792  rescncf  24823  htpyco1  24910  tcphcph  25170  rrxdsfival  25346  ehl2eudisval  25356  volun  25479  dyadval  25526  dvlip  25931  ftc1a  25977  ftc2ditglem  25985  tdeglem3  25997  q1pval  26093  reefgim  26393  relogoprlem  26533  eflogeq  26544  zetacvg  26958  lgsdir2  27274  lgsdchr  27299  2sq2  27377  2sqnn0  27382  negsdi  27996  brbtwn2  28885  ax5seglem4  28912  axeuclid  28943  axcontlem2  28945  axcontlem4  28947  axcontlem8  28951  clwwlknccat  30042  ex-fpar  30441  ipasslem11  30819  hhssnv  31243  mayete3i  31707  idunop  31957  idhmop  31961  0lnfn  31964  lnopmi  31979  lnophsi  31980  lnopcoi  31982  hmops  31999  hmopm  32000  nlelshi  32039  cnlnadjlem2  32047  kbass6  32100  strlem3a  32231  hstrlem3a  32239  elrgspnlem2  33210  mndpluscn  33909  xrge0iifhom  33920  rezh  33952  probdsb  34406  resconn  35226  iscvm  35239  satfdmlem  35348  satffunlem1lem1  35382  satffunlem2lem1  35384  fwddifnval  36144  bj-bary1  37293  poimirlem15  37622  mbfposadd  37654  ftc1anclem3  37682  rrnmval  37815  dvhopaddN  41101  nnadddir  42251  cnreeu  42471  prjcrvfval  42612  pellex  42816  rmxfval  42885  rmyfval  42886  qirropth  42889  rmxycomplete  42899  jm2.15nn0  42985  rmxdioph  42998  expdiophlem2  43004  mendvsca  43169  deg1mhm  43182  mnringmulrvald  44209  addrval  44448  subrval  44449  fmulcl  45572  fmuldfeqlem1  45573  line  48714  itsclc0xyqsolr  48751