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

Theorem oveqan12d 5443
Description: Equality deduction for operation value. (Contributed by NM, 10-Aug-1995.)
Hypotheses
Ref Expression
oveq1d.1 (φA = B)
opreqan12i.2 (ψ𝐶 = 𝐷)
Assertion
Ref Expression
oveqan12d ((φ ψ) → (A𝐹𝐶) = (B𝐹𝐷))

Proof of Theorem oveqan12d
StepHypRef Expression
1 oveq1d.1 . 2 (φA = B)
2 opreqan12i.2 . 2 (ψ𝐶 = 𝐷)
3 oveq12 5433 . 2 ((A = B 𝐶 = 𝐷) → (A𝐹𝐶) = (B𝐹𝐷))
41, 2, 3syl2an 273 1 ((φ ψ) → (A𝐹𝐶) = (B𝐹𝐷))
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97   = wceq 1223  (class class class)co 5424
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 614  ax-5 1309  ax-7 1310  ax-gen 1311  ax-ie1 1355  ax-ie2 1356  ax-8 1368  ax-10 1369  ax-11 1370  ax-i12 1371  ax-bnd 1372  ax-4 1373  ax-17 1392  ax-i9 1396  ax-ial 1400  ax-i5r 1401  ax-ext 1995
This theorem depends on definitions:  df-bi 110  df-3an 869  df-tru 1226  df-nf 1323  df-sb 1619  df-clab 2000  df-cleq 2006  df-clel 2009  df-nfc 2140  df-rex 2281  df-v 2528  df-un 2890  df-sn 3345  df-pr 3346  df-op 3348  df-uni 3544  df-br 3728  df-iota 4782  df-fv 4825  df-ov 5427
This theorem is referenced by:  oveqan12rd  5444  offval  5630  offval3  5672  ecovdi  6116  ecovidi  6117  distrpig  6179  addcmpblnq  6212  addpipqqs  6215  mulpipq  6217  addcomnqg  6226  addcmpblnq0  6284  distrnq0  6300  recexprlem1ssl  6454  recexprlem1ssu  6455  1idsr  6506  addcnsrec  6548  mulcnsrec  6549  mulid1  6625  mulsub  6997  mulsub2  6998  muleqadd  7234  divmuldivap  7273  addltmul  7739
  Copyright terms: Public domain W3C validator