| 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 216 | . . 3 ⊢ (𝜑 → 𝜓) |
| 3 | 2 | sbimi 2074 | . 2 ⊢ ([𝑡 / 𝑥]𝜑 → [𝑡 / 𝑥]𝜓) |
| 4 | 1 | biimpri 228 | . . 3 ⊢ (𝜓 → 𝜑) |
| 5 | 4 | sbimi 2074 | . 2 ⊢ ([𝑡 / 𝑥]𝜓 → [𝑡 / 𝑥]𝜑) |
| 6 | 3, 5 | impbii 209 | 1 ⊢ ([𝑡 / 𝑥]𝜑 ↔ [𝑡 / 𝑥]𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 [wsb 2064 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 |
| This theorem depends on definitions: df-bi 207 df-sb 2065 |
| This theorem is referenced by: 2sbbii 2077 sb3an 2081 sbcom4 2089 sbievw2 2098 cbvsbv 2100 sbco4lemOLD 2174 sbco4OLD 2175 sbcovOLD 2257 sbex 2281 sbor 2307 sbbi 2308 sbnf 2312 sbnfOLD 2313 sbco 2512 sbidm 2515 sbco2d 2517 sbco3 2518 sb7f 2530 sbmo 2614 cbvab 2814 clelsb2OLD 2870 clelsb1fw 2909 clelsb1f 2910 sbabel 2938 sbabelOLD 2939 sbralie 3358 sbralieALT 3359 sbccow 3811 sbcco 3814 exss 5468 inopab 5839 difopab 5840 isarep1OLD 6657 xpab 35726 bj-sbeq 36902 bj-snsetex 36964 2uasbanh 44581 2uasbanhVD 44931 2reu8i 47125 ichv 47436 ichf 47437 ichid 47438 ichcircshi 47441 ichan 47442 ichn 47443 ichbi12i 47447 icheq 47449 ichal 47453 ichnreuop 47459 ichreuopeq 47460 |
| Copyright terms: Public domain | W3C validator |