Theorem opreq12 4028

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

Syntax hints:   -> wi 3   /\ wa 230   = wceq 997  (class class class)co 4021

This theorem is referenced by:  opreqan12d 4037  oev2 4220  oa00 4251  ecopopreq 4369  ecopoprtrn 4372  th3qlem1 4375  th3qlem2 4376  mulcmpblnq 5118  addpipq 5119  mulpipq 5120  ordpipq 5121  halfpq 5147  genpv 5167  genpprecl 5169  distrlem5pr 5196  addcmpblnr 5246  addsrpr 5249  mulsrpr 5250  ltsrpr 5251  mulgt0sr 5279  ssgt0sr 5282  subid 5460  1re 5500  addge0i 5664  recextlem2 5748  lt2msq 5946  le2msq 5963  nn0addcl 6202  qaddcl 6321  qmulcl 6323  fzopth 6528  nn0opthi 6756  sqr0 6762  sqrlem4 6766  sqrlem6 6768  sqrlem12 6774  sqrlem21 6783  sqrlem22 6784  sqrlem24 6786  sqrgt0ii 6787  sqrlem26 6788  sqr11i 6793  faclbnd 7035  faclbnd3 7037  bccl2 7061  fsum1slem 7098  bcxmaslem1 7164  2climnni 7192  2climnn0i 7193  fsum0diag 7348  acdc2 7582  acdc5 7585  tgioolem 7999  ablsn 8209  ring2 8233  ringsn 8247  hmoval 8554  normval 9073  hsn0elch 9203  ocsh 9239  shscli 9364  shs00i 9456  chj00i 9493  riesz4i 10079  hmopidmchi 10162  stm1addi 10256  stm1add3i 10258  superpos 10365  ghomgrpilem2 10471  ghomsn 10473

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-8 1005  ax-10 1007  ax-11 1008  ax-12 1009  ax-13 1010  ax-14 1011  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019  ax-9o 1164  ax-10o 1182  ax-16 1252  ax-11o 1260  ax-ext 1504  ax-sep 2758  ax-pow 2798  ax-pr 2835

This theorem depends on definitions:  df-bi 154  df-or 231  df-an 232  df-ex 1022  df-sb 1214  df-eu 1424  df-mo 1425  df-clab 1510  df-cleq 1515  df-clel 1518  df-ne 1634  df-v 1859  df-dif 2100  df-un 2101  df-in 2102  df-ss 2104  df-nul 2332  df-pw 2454  df-sn 2464  df-pr 2465  df-op 2468  df-uni 2558  df-br 2675  df-opab 2722  df-xp 3241  df-cnv 3243  df-dm 3245  df-rn 3246  df-res 3247  df-ima 3248  df-fv 3255  df-opr 4023

Copyright terms: Public domain