![]() |
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 215 | . . 3 ⊢ (𝜑 → 𝜓) |
3 | 2 | sbimi 2070 | . 2 ⊢ ([𝑡 / 𝑥]𝜑 → [𝑡 / 𝑥]𝜓) |
4 | 1 | biimpri 227 | . . 3 ⊢ (𝜓 → 𝜑) |
5 | 4 | sbimi 2070 | . 2 ⊢ ([𝑡 / 𝑥]𝜓 → [𝑡 / 𝑥]𝜑) |
6 | 3, 5 | impbii 208 | 1 ⊢ ([𝑡 / 𝑥]𝜑 ↔ [𝑡 / 𝑥]𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 [wsb 2060 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 |
This theorem depends on definitions: df-bi 206 df-sb 2061 |
This theorem is referenced by: 2sbbii 2073 sb3an 2077 sbcom4 2085 sbievw2 2092 sbco4lem 2164 sbco4 2165 sbcov 2244 sbco4lemOLD 2268 sbex 2271 sbor 2297 sbbi 2298 sbnf 2302 sbnfOLD 2303 cbvsbv 2354 sbco 2501 sbidm 2504 sbco2d 2506 sbco3 2507 sb7f 2519 sbmo 2603 cbvab 2801 clelsb2OLD 2855 clelsb1fw 2896 clelsb1f 2897 sbabel 2928 sbabelOLD 2929 sbralie 3342 sbralieALT 3343 sbccow 3799 sbcco 3802 exss 5469 inopab 5835 difopab 5836 isarep1OLD 6649 xpab 35548 bj-sbeq 36607 bj-snsetex 36670 2uasbanh 44237 2uasbanhVD 44587 2reu8i 46726 ichv 47021 ichf 47022 ichid 47023 ichcircshi 47026 ichan 47027 ichn 47028 ichbi12i 47032 icheq 47034 ichal 47038 ichnreuop 47044 ichreuopeq 47045 |
Copyright terms: Public domain | W3C validator |