![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sbbii | Structured version Visualization 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 198 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | sbimi 1803 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1 | biimpri 210 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() |
5 | 4 | sbimi 1803 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 3, 5 | impbii 191 |
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 1669 ax-4 1682 |
This theorem depends on definitions: df-bi 189 df-an 373 df-ex 1664 df-sb 1798 |
This theorem is referenced by: sbor 2227 sban 2228 sb3an 2229 sbbi 2230 sbco 2241 sbidm 2243 sbco2d 2245 sbco3 2246 equsb3 2261 equsb3ALT 2262 elsb3 2263 elsb4 2264 sbcom4 2275 sb7f 2282 sbex 2292 sbco4lem 2294 sbco4 2295 sbmo 2344 eqsb3 2556 clelsb3 2557 cbvab 2574 sbabel 2620 sbabelOLD 2621 sbralie 3032 sbcco 3290 exss 4663 inopab 4965 isarep1 5662 clelsb3f 28116 bj-sbnf 31441 bj-clelsb3 31457 bj-sbeq 31503 bj-snsetex 31557 2uasbanh 36928 2uasbanhVD 37308 |
Copyright terms: Public domain | W3C validator |