![]() |
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 217 | . . 3 ⊢ (𝜑 → 𝜓) |
3 | 2 | sbimi 2050 | . 2 ⊢ ([𝑡 / 𝑥]𝜑 → [𝑡 / 𝑥]𝜓) |
4 | 1 | biimpri 229 | . . 3 ⊢ (𝜓 → 𝜑) |
5 | 4 | sbimi 2050 | . 2 ⊢ ([𝑡 / 𝑥]𝜓 → [𝑡 / 𝑥]𝜑) |
6 | 3, 5 | impbii 210 | 1 ⊢ ([𝑡 / 𝑥]𝜑 ↔ [𝑡 / 𝑥]𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 [wsb 2040 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1775 ax-4 1789 |
This theorem depends on definitions: df-bi 208 df-sb 2041 |
This theorem is referenced by: 2sbbii 2053 sb3an 2058 sbcom4 2068 sbievw2 2072 equsb3rOLD 2076 sbcov 2219 sbco4lem 2247 sbco4 2248 sbex 2252 sbanOLD 2276 sbor 2279 sbbi 2280 sbanvOLD 2289 sbbivOLD 2290 sbco 2501 sbidm 2504 sbco2d 2506 sbco3 2507 sb7f 2519 sbmo 2664 clelsb3vOLD 2909 cbvabv 2925 cbvab 2926 clelsb3f 2951 clelsb3fOLD 2952 sbabel 2981 sbralie 3414 sbcco 3724 exss 5240 inopab 5579 isarep1 6304 bj-sbnf 33678 bj-sbeq 33733 bj-snsetex 33826 wl-clelsb3df 34340 2uasbanh 40386 2uasbanhVD 40736 2reu8i 42782 ichv 43045 ichf 43046 ichid 43047 ichcircshi 43048 ichbi12i 43054 icheq 43056 ichn 43062 ichal 43063 ichan 43066 ichnreuop 43070 ichreuopeq 43071 |
Copyright terms: Public domain | W3C validator |