ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  oveq12 Unicode version

Theorem oveq12 5751
Description: Equality theorem for operation value. (Contributed by NM, 16-Jul-1995.)
Assertion
Ref Expression
oveq12  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A F C )  =  ( B F D ) )

Proof of Theorem oveq12
StepHypRef Expression
1 oveq1 5749 . 2  |-  ( A  =  B  ->  ( A F C )  =  ( B F C ) )
2 oveq2 5750 . 2  |-  ( C  =  D  ->  ( B F C )  =  ( B F D ) )
31, 2sylan9eq 2170 1  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A F C )  =  ( B F D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    = wceq 1316  (class class class)co 5742
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-3an 949  df-tru 1319  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-rex 2399  df-v 2662  df-un 3045  df-sn 3503  df-pr 3504  df-op 3506  df-uni 3707  df-br 3900  df-iota 5058  df-fv 5101  df-ov 5745
This theorem is referenced by:  oveq12i  5754  oveq12d  5760  oveqan12d  5761  ecopoveq  6492  ecopovtrn  6494  ecopovtrng  6497  th3qlem1  6499  th3qlem2  6500  mulcmpblnq  7144  addpipqqs  7146  ordpipqqs  7150  enq0breq  7212  mulcmpblnq0  7220  nqpnq0nq  7229  nqnq0a  7230  nqnq0m  7231  nq0m0r  7232  nq0a0  7233  distrlem5prl  7362  distrlem5pru  7363  addcmpblnr  7515  ltsrprg  7523  mulgt0sr  7554  add20  8204  cru  8332  qaddcl  9395  qmulcl  9397  xaddval  9596  xnn0xadd0  9618  fzopth  9809  modqval  10065  seqvalcd  10200  seqovcd  10204  1exp  10290  m1expeven  10308  nn0opthd  10436  faclbnd  10455  faclbnd3  10457  bcn0  10469  reval  10589  absval  10741  clim  11018  fsumparts  11207  dvds2add  11454  dvds2sub  11455  opoe  11519  omoe  11520  opeo  11521  omeo  11522  gcddvds  11579  gcdcl  11582  gcdeq0  11592  gcdneg  11597  gcdaddm  11599  gcdabs  11603  gcddiv  11634  eucalgval2  11661  lcmabs  11684  rpmul  11706  divgcdcoprmex  11710  prmexpb  11756  rpexp  11758  nn0gcdsq  11805  cnmpt2t  12389  cnmpt22f  12391  hmeofvalg  12399  bdmetval  12596
  Copyright terms: Public domain W3C validator