Theorem opreq12 3976

Description: Equality theorem for operation value.

Assertion

Ref	Expression
opreq12	|- ((A = B /\ C = D) -> (AFC) = (BFD))

Proof of Theorem opreq12

Step	Hyp	Ref	Expression
1		opreq1 3974	. 2 |- (A = B -> (AFC) = (BFC))
2		opreq2 3975	. 2 |- (C = D -> (BFC) = (BFD))
3	1, 2	sylan9eq 1530	1 |- ((A = B /\ C = D) -> (AFC) = (BFD))

Syntax hints:   -> wi 3   /\ wa 223   = wceq 958  (class class class)co 3969

This theorem is referenced by:  opreqan12d 3985  oev2 4168  oa00 4199  ecopopreq 4314  ecopoprtrn 4317  th3qlem1 4320  th3qlem2 4321  mulcmpblnq 5065  addpipq 5066  mulpipq 5067  ordpipq 5068  halfpq 5094  genpv 5114  genpprecl 5116  distrlem5pr 5143  addcmpblnr 5193  addsrpr 5196  mulsrpr 5197  ltsrpr 5198  mulgt0sr 5226  ssgt0sr 5229  subidt 5407  1re 5447  addge0 5611  recextlem2 5695  lt2msqt 5888  le2msqt 5905  nn0addclt 6122  qaddclt 6270  qmulclt 6272  fzoptht 6503  nn0opth 6667  sqr0 6673  sqrlem4 6677  sqrlem6 6679  sqrlem12 6685  sqrlem21 6694  sqrlem22 6695  sqrlem24 6697  sqrgt0i 6698  sqrlem26 6699  sqr11 6704  faclbnd 6945  faclbnd3 6947  bccl2t 6971  fsum1slem 7008  bcxmaslem1 7074  2climnn 7102  2climnn0 7103  fsum0diag 7258  acdc2 7491  acdc5 7494  tgioolem 7911  ablsn 8121  ring2 8145  ringsn 8159  hmoval 8466  normvalt 8985  hsn0elch 9115  ocsh 9151  shscl 9276  shs00 9368  chj00 9405  riesz4 9991  hmopidmch 10074  stm1add 10167  stm1add3 10169  superpos 10276  ghomgrpilem2 10381  ghomsn 10383

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-11 969  ax-12 970  ax-13 971  ax-14 972  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462  ax-sep 2708  ax-pow 2748  ax-pr 2785

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 983  df-sb 1174  df-eu 1384  df-mo 1385  df-clab 1467  df-cleq 1472  df-clel 1475  df-ne 1590  df-v 1815  df-dif 2052  df-un 2053  df-in 2054  df-ss 2056  df-nul 2284  df-pw 2406  df-sn 2416  df-pr 2417  df-op 2420  df-uni 2508  df-br 2625  df-opab 2672  df-xp 3190  df-cnv 3192  df-dm 3194  df-rn 3195  df-res 3196  df-ima 3197  df-fv 3204  df-opr 3971

Copyright terms: Public domain