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 206 | . . 3 |
3 | 2 | sbimi 1886 | . 2 |
4 | 1 | biimpri 218 | . . 3 |
5 | 4 | sbimi 1886 | . 2 |
6 | 3, 5 | impbii 199 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wb 196 wsb 1880 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 |
This theorem depends on definitions: df-bi 197 df-an 386 df-ex 1705 df-sb 1881 |
This theorem is referenced by: sbor 2398 sban 2399 sb3an 2400 sbbi 2401 sbco 2412 sbidm 2414 sbco2d 2416 sbco3 2417 equsb3 2432 equsb3ALT 2433 elsb3 2434 elsb4 2435 sbcom4 2446 sb7f 2453 sbex 2463 sbco4lem 2465 sbco4 2466 sbmo 2515 eqsb3 2728 clelsb3 2729 cbvab 2746 clelsb3f 2768 sbabel 2793 sbralie 3184 sbcco 3458 exss 4931 inopab 5252 isarep1 5977 bj-sbnf 32828 bj-clelsb3 32848 bj-sbeq 32896 bj-snsetex 32951 2uasbanh 38777 2uasbanhVD 39147 |
Copyright terms: Public domain | W3C validator |