MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sbequ12r Unicode version

Theorem sbequ12r 1993
Description: An equality theorem for substitution. (Contributed by NM, 6-Oct-2004.) (Proof shortened by Andrew Salmon, 21-Jun-2011.)
Assertion
Ref Expression
sbequ12r

Proof of Theorem sbequ12r
StepHypRef Expression
1 sbequ12 1992 . . 3
21bicomd 201 . 2
32equcoms 1795 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  [wsb 1739
This theorem is referenced by:  sbequ12a  1994  sbid  1996  sbidmOLD  2157  sb5rf  2165  sb6rf  2166  2sb5rf  2195  2sb6rf  2196  abbiOLD  2589  opeliunxp  5056  isarep1  5672  findes  6730  axrepndlem1  8988  axrepndlem2  8989  nn0min  27611  esumcvg  28092  wl-nfs1t  29991  wl-sb6rft  29997  wl-equsb4  30005  wl-ax11-lem5  30029  sbcalf  30517  sbcexf  30518  opeliun2xp  32922  bj-abbi  34361
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-12 1854
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-sb 1740
  Copyright terms: Public domain W3C validator