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

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

Proof of Theorem sbbii
StepHypRef Expression
1 sbbii.1 . . . 4
21biimpi 113 . . 3
32sbimi 1644 . 2
41biimpri 124 . . 3
54sbimi 1644 . 2
63, 5impbii 117 1
Colors of variables: wff set class
Syntax hints:   wb 98  wsb 1642
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-5 1333  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-4 1397  ax-ial 1424
This theorem depends on definitions:  df-bi 110  df-sb 1643
This theorem is referenced by:  sbco2v  1818  equsb3  1822  sbn  1823  sbim  1824  sbor  1825  sban  1826  sb3an  1829  sbbi  1830  sbco2h  1835  sbco2d  1837  sbco2vd  1838  sbco3v  1840  sbco3  1845  elsb3  1849  elsb4  1850  sbcom2v2  1859  sbcom2  1860  dfsb7  1864  sb7f  1865  sb7af  1866  sbal  1873  sbal1  1875  sbex  1877  sbco4lem  1879  sbco4  1880  sbmo  1956  eqsb3  2138  clelsb3  2139  clelsb4  2140  sbabel  2200  sbralie  2540  sbcco  2779  exss  3954  inopab  4411  isarep1  4928
  Copyright terms: Public domain W3C validator