![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sbbii | Structured version Visualization version GIF 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 1943 | . 2 ⊢ ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓) |
4 | 1 | biimpri 218 | . . 3 ⊢ (𝜓 → 𝜑) |
5 | 4 | sbimi 1943 | . 2 ⊢ ([𝑦 / 𝑥]𝜓 → [𝑦 / 𝑥]𝜑) |
6 | 3, 5 | impbii 199 | 1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 [wsb 1937 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 |
This theorem depends on definitions: df-bi 197 df-an 385 df-ex 1745 df-sb 1938 |
This theorem is referenced by: sbor 2426 sban 2427 sb3an 2428 sbbi 2429 sbco 2440 sbidm 2442 sbco2d 2444 sbco3 2445 equsb3 2460 equsb3ALT 2461 elsb3 2462 elsb4 2463 sbcom4 2474 sb7f 2481 sbex 2491 sbco4lem 2493 sbco4 2494 sbmo 2544 eqsb3 2757 clelsb3 2758 cbvab 2775 clelsb3f 2797 sbabel 2822 sbralie 3214 sbcco 3491 exss 4961 inopab 5285 isarep1 6015 bj-sbnf 32953 bj-clelsb3 32973 bj-sbeq 33021 bj-snsetex 33076 2uasbanh 39094 2uasbanhVD 39461 |
Copyright terms: Public domain | W3C validator |