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

Theorem sbbii 1746
Description: Infer substitution into both sides of a logical equivalence. (Contributed by NM, 14-May-1993.)
Hypothesis
Ref Expression
sbbii.1
Assertion
Ref Expression
sbbii

Proof of Theorem sbbii
StepHypRef Expression
1 sbbii.1 . . . 4
21biimpi 194 . . 3
32sbimi 1745 . 2
41biimpri 206 . . 3
54sbimi 1745 . 2
63, 5impbii 188 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  [wsb 1739
This theorem is referenced by:  sbor  2139  sban  2140  sb3an  2141  sbbi  2142  sbco  2154  sbidm  2156  sbco2d  2159  sbco3  2160  equsb3  2176  equsb3ALT  2177  elsb3  2178  elsb4  2179  sbcom4  2190  sb7f  2197  sbex  2207  sbco4lem  2209  sbco4  2210  sbmo  2335  2eu6OLD  2384  eqsb3  2577  clelsb3  2578  cbvab  2598  sbabel  2650  sbabelOLD  2651  sbralie  3097  sbcco  3350  exss  4715  inopab  5138  isarep1  5672  clelsb3f  27379  2uasbanh  33334  2uasbanhVD  33711  bj-sbnf  34412  bj-clelsb3  34424  bj-sbeq  34468  bj-snsetex  34521  frege72  37963
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-sb 1740
  Copyright terms: Public domain W3C validator