Theorem oveqan12d 6669

Description: Equality deduction for operation value. (Contributed by NM, 10-Aug-1995.)

Hypotheses

Ref	Expression
oveq1d.1	|- ( ph -> A = B )
opreqan12i.2	|- ( ps -> C = D )

Assertion

Ref	Expression
oveqan12d	|- ( ( ph /\ ps ) -> ( A F C ) = ( B F D ) )

Proof of Theorem oveqan12d

Step	Hyp	Ref	Expression
1		oveq1d.1	. 2 |- ( ph -> A = B )
2		opreqan12i.2	. 2 |- ( ps -> C = D )
3		oveq12 6659	. 2 |- ( ( A = B /\ C = D ) -> ( A F C ) = ( B F D ) )
4	1, 2, 3	syl2an 494	1 |- ( ( ph /\ ps ) -> ( A F C ) = ( B F D ) )

Syntax hints:   -> wi 4   /\ wa 384   = wceq 1483  (class class class)co 6650

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-ov 6653

This theorem is referenced by:  oveqan12rd  6670  offval  6904  offval3  7162  odi  7659  omopth2  7664  oeoa  7677  ecovdi  7856  ackbij1lem9  9050  alephadd  9399  distrpi  9720  addpipq  9759  mulpipq  9762  lterpq  9792  reclem3pr  9871  1idsr  9919  mulcnsr  9957  mulid1  10037  1re  10039  mul02  10214  addcom  10222  mulsub  10473  mulsub2  10474  muleqadd  10671  divmuldiv  10725  div2sub  10850  addltmul  11268  xnegdi  12078  xadddilem  12124  fzsubel  12377  fzoval  12471  seqid3  12845  mulexp  12899  sqdiv  12928  hashdom  13168  hashun  13171  ccatfval  13358  splcl  13503  crim  13855  readd  13866  remullem  13868  imadd  13874  cjadd  13881  cjreim  13900  sqrtmul  14000  sqabsadd  14022  sqabssub  14023  absmul  14034  abs2dif  14072  binom  14562  binomfallfac  14772  sinadd  14894  cosadd  14895  dvds2ln  15014  sadcaddlem  15179  bezoutlem4  15259  bezout  15260  absmulgcd  15266  gcddiv  15268  bezoutr1  15282  lcmgcd  15320  lcmfass  15359  nn0gcdsq  15460  crth  15483  pythagtriplem1  15521  pcqmul  15558  4sqlem4a  15655  4sqlem4  15656  prdsplusgval  16133  prdsmulrval  16135  prdsdsval  16138  prdsvscaval  16139  xpsfval  16227  xpsval  16232  idmhm  17344  0mhm  17358  resmhm  17359  prdspjmhm  17367  pwsdiagmhm  17369  gsumws2  17379  frmdup1  17401  eqgval  17643  idghm  17675  resghm  17676  mulgmhm  18233  mulgghm  18234  srglmhm  18535  srgrmhm  18536  ringlghm  18604  ringrghm  18605  gsumdixp  18609  isrhm  18721  issrngd  18861  lmodvsghm  18924  pwssplit2  19060  asclghm  19338  psrmulfval  19385  evlslem4  19508  mpfrcl  19518  xrsdsval  19790  expmhm  19815  expghm  19844  mulgghm2  19845  mulgrhm  19846  cygznlem3  19918  mamuval  20192  mamufv  20193  mvmulval  20349  mndifsplit  20442  mat2pmatmul  20536  decpmatmul  20577  fmval  21747  fmf  21749  flffval  21793  divcn  22671  rescncf  22700  htpyco1  22777  tchcph  23036  volun  23313  dyadval  23360  dvlip  23756  ftc1a  23800  ftc2ditglem  23808  tdeglem3  23819  q1pval  23913  reefgim  24204  relogoprlem  24337  eflogeq  24348  zetacvg  24741  lgsdir2  25055  lgsdchr  25080  brbtwn2  25785  ax5seglem4  25812  axeuclid  25843  axcontlem2  25845  axcontlem4  25847  axcontlem8  25851  numclwlk1lem2fo  27228  ipasslem11  27695  hhssnv  28121  mayete3i  28587  idunop  28837  idhmop  28841  0lnfn  28844  lnopmi  28859  lnophsi  28860  lnopcoi  28862  hmops  28879  hmopm  28880  nlelshi  28919  cnlnadjlem2  28927  kbass6  28980  strlem3a  29111  hstrlem3a  29119  bhmafibid1  29644  mndpluscn  29972  xrge0iifhom  29983  rezh  30015  probdsb  30484  resconn  31228  iscvm  31241  fwddifnval  32270  bj-bary1  33162  poimirlem15  33424  mbfposadd  33457  ftc1anclem3  33487  rrnmval  33627  dvhopaddN  36403  pellex  37399  rmxfval  37468  rmyfval  37469  qirropth  37473  rmxycomplete  37482  jm2.15nn0  37570  rmxdioph  37583  expdiophlem2  37589  mendvsca  37761  deg1mhm  37785  addrval  38670  subrval  38671  fmulcl  39813  fmuldfeqlem1  39814  idmgmhm  41788  resmgmhm  41798  rhmval  41919  offval0  42299