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

Theorem oveq12 5549
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 5547 . 2  |-  ( A  =  B  ->  ( A F C )  =  ( B F C ) )
2 oveq2 5548 . 2  |-  ( C  =  D  ->  ( B F C )  =  ( B F D ) )
31, 2sylan9eq 2108 1  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A F C )  =  ( B F D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101    = wceq 1259  (class class class)co 5540
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-3an 898  df-tru 1262  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-rex 2329  df-v 2576  df-un 2950  df-sn 3409  df-pr 3410  df-op 3412  df-uni 3609  df-br 3793  df-iota 4895  df-fv 4938  df-ov 5543
This theorem is referenced by:  oveq12i  5552  oveq12d  5558  oveqan12d  5559  sprmpt2  5888  ecopoveq  6232  ecopovtrn  6234  ecopovtrng  6237  th3qlem1  6239  th3qlem2  6240  mulcmpblnq  6524  addpipqqs  6526  ordpipqqs  6530  enq0breq  6592  mulcmpblnq0  6600  nqpnq0nq  6609  nqnq0a  6610  nqnq0m  6611  nq0m0r  6612  nq0a0  6613  distrlem5prl  6742  distrlem5pru  6743  addcmpblnr  6882  ltsrprg  6890  mulgt0sr  6920  add20  7543  cru  7667  qaddcl  8667  qmulcl  8669  fzopth  9026  modqval  9274  1exp  9449  m1expeven  9467  nn0opthd  9590  faclbnd  9609  faclbnd3  9611  bcn0  9623  reval  9677  absval  9828  clim  10033  dvds2add  10141  dvds2sub  10142  opoe  10207  omoe  10208  opeo  10209  omeo  10210
  Copyright terms: Public domain W3C validator