Theorem oveq12 5783

Description: Equality theorem for operation value. (Contributed by NM, 16-Jul-1995.)

Assertion

Ref	Expression
oveq12	⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))

Proof of Theorem oveq12

Step	Hyp	Ref	Expression
1		oveq1 5781	. 2 ⊢ (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))
2		oveq2 5782	. 2 ⊢ (𝐶 = 𝐷 → (𝐵𝐹𝐶) = (𝐵𝐹𝐷))
3	1, 2	sylan9eq 2192	1 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))

Syntax hints:   → wi 4   ∧ wa 103   = wceq 1331  (class class class)co 5774

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 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-rex 2422  df-v 2688  df-un 3075  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-br 3930  df-iota 5088  df-fv 5131  df-ov 5777

This theorem is referenced by:  oveq12i  5786  oveq12d  5792  oveqan12d  5793  ecopoveq  6524  ecopovtrn  6526  ecopovtrng  6529  th3qlem1  6531  th3qlem2  6532  mulcmpblnq  7176  addpipqqs  7178  ordpipqqs  7182  enq0breq  7244  mulcmpblnq0  7252  nqpnq0nq  7261  nqnq0a  7262  nqnq0m  7263  nq0m0r  7264  nq0a0  7265  distrlem5prl  7394  distrlem5pru  7395  addcmpblnr  7547  ltsrprg  7555  mulgt0sr  7586  add20  8236  cru  8364  qaddcl  9427  qmulcl  9429  xaddval  9628  xnn0xadd0  9650  fzopth  9841  modqval  10097  seqvalcd  10232  seqovcd  10236  1exp  10322  m1expeven  10340  nn0opthd  10468  faclbnd  10487  faclbnd3  10489  bcn0  10501  reval  10621  absval  10773  clim  11050  fsumparts  11239  dvds2add  11527  dvds2sub  11528  opoe  11592  omoe  11593  opeo  11594  omeo  11595  gcddvds  11652  gcdcl  11655  gcdeq0  11665  gcdneg  11670  gcdaddm  11672  gcdabs  11676  gcddiv  11707  eucalgval2  11734  lcmabs  11757  rpmul  11779  divgcdcoprmex  11783  prmexpb  11829  rpexp  11831  nn0gcdsq  11878  cnmpt2t  12462  cnmpt22f  12464  hmeofvalg  12472  bdmetval  12669