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 1570	1 |- ((A = B /\ C = D) -> (AFC) = (BFD))

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

This theorem is referenced by:  opreqan12d 4037  oev2 4298  oa00 4329  ecopopreq 4449  ecopoprtrn 4452  th3qlem1 4455  th3qlem2 4456  mulcmpblnq 5207  addpipq 5208  mulpipq 5209  ordpipq 5210  halfpq 5236  genpv 5256  genpprecl 5258  distrlem5pr 5285  addcmpblnr 5335  addsrpr 5338  mulsrpr 5339  ltsrpr 5340  mulgt0sr 5368  ssgt0sr 5371  subid 5549  1re 5589  addge0i 5753  recextlem2 5839  lt2msq 6031  le2msq 6048  nn0addcl 6288  qaddcl 6408  qmulcl 6410  fzopth 6632  nn0opthi 6867  sqr0 6873  sqrlem4 6877  sqrlem6 6879  sqrlem12 6885  sqrlem21 6894  sqrlem22 6895  sqrlem24 6897  sqrgt0ii 6898  sqrlem26 6899  sqr11i 6904  faclbnd 7148  faclbnd3 7150  bccl2 7174  fsum1slem 7211  bcxmaslem1 7277  2climnn 7305  2climnn0 7306  fsum0diag 7463  acdc2 7702  acdc5 7705  tgioolem 8125  ablsn 8366  ring2 8391  ringsn 8405  hmoval 8725  normval 9266  hsn0elch 9396  ocsh 9432  shscli 9557  shs00i 9649  chj00i 9686  riesz4i 10275  hmopidmchi 10359  stm1addi 10453  stm1add3i 10455  superpos 10562  ghomgrpilem2 10671  ghomsn 10673  altretop 11144  idsubfun 11312  bfplem9 12062

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-11 1003  ax-12 1004  ax-13 1005  ax-14 1006  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500  ax-sep 2777  ax-pow 2818  ax-pr 2855

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1017  df-sb 1209  df-eu 1421  df-mo 1422  df-clab 1506  df-cleq 1511  df-clel 1514  df-ne 1630  df-v 1858  df-dif 2101  df-un 2102  df-in 2103  df-ss 2105  df-nul 2333  df-pw 2459  df-sn 2470  df-pr 2471  df-op 2474  df-uni 2570  df-br 2693  df-opab 2741  df-xp 3265  df-cnv 3267  df-dm 3269  df-rn 3270  df-res 3271  df-ima 3272  df-fv 3279  df-opr 4023

Copyright terms: Public domain