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

Theorem oveq12 5441
Description: Equality theorem for operation value. (Contributed by NM, 16-Jul-1995.)
Assertion
Ref Expression
oveq12 ((A = B 𝐶 = 𝐷) → (A𝐹𝐶) = (B𝐹𝐷))

Proof of Theorem oveq12
StepHypRef Expression
1 oveq1 5439 . 2 (A = B → (A𝐹𝐶) = (B𝐹𝐶))
2 oveq2 5440 . 2 (𝐶 = 𝐷 → (B𝐹𝐶) = (B𝐹𝐷))
31, 2sylan9eq 2070 1 ((A = B 𝐶 = 𝐷) → (A𝐹𝐶) = (B𝐹𝐷))
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97   = wceq 1226  (class class class)co 5432
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 617  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-8 1372  ax-10 1373  ax-11 1374  ax-i12 1375  ax-bnd 1376  ax-4 1377  ax-17 1396  ax-i9 1400  ax-ial 1405  ax-i5r 1406  ax-ext 2000
This theorem depends on definitions:  df-bi 110  df-3an 873  df-tru 1229  df-nf 1326  df-sb 1624  df-clab 2005  df-cleq 2011  df-clel 2014  df-nfc 2145  df-rex 2286  df-v 2533  df-un 2895  df-sn 3352  df-pr 3353  df-op 3355  df-uni 3551  df-br 3735  df-iota 4790  df-fv 4833  df-ov 5435
This theorem is referenced by:  oveq12i  5444  oveq12d  5450  oveqan12d  5451  sprmpt2  5775  ecopoveq  6108  ecopovtrn  6110  ecopovtrng  6113  th3qlem1  6115  th3qlem2  6116  mulcmpblnq  6221  addpipqqs  6223  ordpipqqs  6227  enq0breq  6285  mulcmpblnq0  6293  nqpnq0nq  6302  nqnq0a  6303  nqnq0m  6304  nq0m0r  6305  nq0a0  6306  distrlem5prl  6419  distrlem5pru  6420  addcmpblnr  6485  ltsrprg  6493  mulgt0sr  6522  add20  7075  cru  7194
  Copyright terms: Public domain W3C validator