![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > sbbii | Structured version Unicode version |
Description: Infer substitution into both sides of a logical equivalence. (Contributed by NM, 14-May-1993.) |
Ref | Expression |
---|---|
sbbii.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
sbbii |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sbbii.1 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | biimpi 194 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | sbimi 1708 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1 | biimpri 206 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() |
5 | 4 | sbimi 1708 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 3, 5 | impbii 188 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 |
This theorem depends on definitions: df-bi 185 df-an 371 df-ex 1588 df-sb 1703 |
This theorem is referenced by: sbnOLD 2093 sbor 2100 sban 2101 sb3an 2102 sbbi 2103 sbco 2116 sbidm 2119 sbco2d 2123 sbco3 2124 sbco3OLD 2125 equsb3 2146 equsb3ALT 2147 elsb3 2148 elsb4 2149 sbcom4 2162 sb7f 2172 sbex 2185 sbco4lem 2187 sbco4 2188 sbmo 2324 2eu6OLD 2381 eqsb3 2574 clelsb3 2575 cbvab 2595 sbabel 2647 sbralie 3066 sbcco 3317 exss 4666 inopab 5081 isarep1 5608 clelsb3f 26036 2uasbanh 31622 2uasbanhVD 31999 bj-sbnf 32699 bj-clelsb3 32711 bj-sbeq 32755 bj-snsetex 32808 |
Copyright terms: Public domain | W3C validator |