Theorem opreq12 3961

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 3959	. 2 |- (A = B -> (AFC) = (BFC))
2		opreq2 3960	. 2 |- (C = D -> (BFC) = (BFD))
3	1, 2	sylan9eq 1524	1 |- ((A = B /\ C = D) -> (AFC) = (BFD))

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

This theorem is referenced by:  opreqan12d 3970  oev2 4152  oa00 4183  ecopopreq 4298  ecopoprtrn 4301  th3qlem1 4304  th3qlem2 4305  mulcmpblnq 5033  addpipq 5034  mulpipq 5035  ordpipq 5036  halfpq 5062  genpv 5082  genpprecl 5084  distrlem5pr 5111  addcmpblnr 5161  addsrpr 5164  mulsrpr 5165  ltsrpr 5166  mulgt0sr 5194  ssgt0sr 5197  subidt 5375  1re 5415  addge0 5581  recextlem2 5664  lt2msqt 5842  le2msqt 5859  nn0addclt 6075  qaddclt 6215  qmulclt 6217  fzoptht 6442  nn0opth 6604  sqr0 6610  sqrlem4 6614  sqrlem6 6616  sqrlem12 6622  sqrlem21 6631  sqrlem22 6632  sqrlem24 6634  sqrgt0i 6635  sqrlem26 6636  sqr11 6641  faclbnd 6890  faclbnd3 6892  bccl2t 6917  fsum1slem 6954  bcxmaslem1 7020  2climnn 7047  2climnn0 7048  fsum0diag 7201  acdc2 7440  acdc5 7443  tgioolem 7866  ablsn 8077  ring2 8101  ringsn 8115  hmoval 8414  circcltOLD 8675  normvalt 8929  hsn0elch 9059  ocsh 9095  shscl 9219  shs00 9311  chj00 9348  riesz4 9934  hmopidmch 10017  stm1add 10110  stm1add3 10112  superpos 10218  ghomgrpilem2 10320  ghomsn 10322

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-11 965  ax-12 966  ax-13 967  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-sep 2698  ax-pow 2737  ax-pr 2774

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-eu 1380  df-mo 1381  df-clab 1462  df-cleq 1467  df-clel 1470  df-ne 1584  df-v 1808  df-dif 2045  df-un 2046  df-in 2047  df-ss 2049  df-nul 2277  df-pw 2398  df-sn 2408  df-pr 2409  df-op 2412  df-uni 2499  df-br 2615  df-opab 2662  df-xp 3179  df-cnv 3181  df-dm 3183  df-rn 3184  df-res 3185  df-ima 3186  df-fv 3193  df-opr 3956

Copyright terms: Public domain