Theorem opreqan12d 4902

Description: Equality deduction for operation value.

Hypotheses

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

Assertion

Ref	Expression
opreqan12d	|- ((ph /\ ps) -> (AFC) = (BFD))

Proof of Theorem opreqan12d

Step	Hyp	Ref	Expression
1		opreq12 4891	. 2 |- ((A = B /\ C = D) -> (AFC) = (BFD))
2		opreq1d.1	. 2 |- (ph -> A = B)
3		opreqan12i.2	. 2 |- (ps -> C = D)
4	1, 2, 3	syl2an 503	1 |- ((ph /\ ps) -> (AFC) = (BFD))

Syntax hints:   -> wi 3   /\ wa 240   = wceq 1298  (class class class)co 4884

This theorem is referenced by:  opreqan12rd 4903  odi 5258  oeoa 5272  ecoprdi 5380  distrpi 6178  addcmpblnq 6204  addpipq 6206  reclem3pr 6310  mulsrpr 6337  1idsr 6359  mulcnsr 6406  addsub4 6640  mulsub 6644  muleqadd 6889  divmuldiv 6956  addltmul 7229  fzsubel 7673  mulexp 7836  sumsqne0i 7879  crui 7987  crne0i 7989  cjreim 8078  cjreim2 8079  sqabsadd 8099  sqabssub 8100  abs2dif 8154  caurei 8179  cauimi 8180  fsumrev 8289  negfcncfi 8531  rescncf 8534  alephadd 8851  metreslem 9099  metcnss2 9177  dscmet 9196  iscaunns 9222  xpcn 9254  iscms2lem3 9269  ghsubgi 9446  va1cnlem 9684  sm1cnilem 9686  lnocoi 9757  ipasslem11 9841  ubthlem8 9879  minveclem18 9907  minveclem19 9908  minveclem21 9910  minveclem36 9925  efgh 10072  relogoprlem 10123  hhssnv 10767  osumlem2 11214  pjvi 11285  mayete3i 11308  mayete3OLDi 11309  idunop 11539  idhmop 11543  0lnfn 11546  lnopmi 11562  lnophsi 11563  lnopcoi 11565  hmops 11582  hmopm 11583  nlelshi 11630  cnlnadjlem2 11638  kbass6 11692  strlem3a 11824  hstrlem3a 11832  ghomsn 13631  dvds2ln 13684  mulgcdlem7 13762  mulgcd 13763  absmulgcd 13764  caures 15852  bfplem11 16008  ismrer1 16024

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-rex 2110  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-xp 4000  df-cnv 4002  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fv 4014  df-opr 4886

Copyright terms: Public domain