![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > sbbii | GIF version |
Description: Infer substitution into both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
sbbii.1 | ⊢ (𝜑 ↔ 𝜓) |
Ref | Expression |
---|---|
sbbii | ⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sbbii.1 | . . . 4 ⊢ (𝜑 ↔ 𝜓) | |
2 | 1 | biimpi 120 | . . 3 ⊢ (𝜑 → 𝜓) |
3 | 2 | sbimi 1775 | . 2 ⊢ ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓) |
4 | 1 | biimpri 133 | . . 3 ⊢ (𝜓 → 𝜑) |
5 | 4 | sbimi 1775 | . 2 ⊢ ([𝑦 / 𝑥]𝜓 → [𝑦 / 𝑥]𝜑) |
6 | 3, 5 | impbii 126 | 1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜓) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 105 [wsb 1773 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1458 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-4 1521 ax-ial 1545 |
This theorem depends on definitions: df-bi 117 df-sb 1774 |
This theorem is referenced by: sbco2vh 1961 equsb3 1967 sbn 1968 sbim 1969 sbor 1970 sban 1971 sb3an 1974 sbbi 1975 sbco2h 1980 sbco2d 1982 sbco2vd 1983 sbco3v 1985 sbco3 1990 sbcom2v2 2002 sbcom2 2003 dfsb7 2007 sb7f 2008 sb7af 2009 sbal 2016 sbal1 2018 sbex 2020 sbco4lem 2022 sbco4 2023 sbmo 2101 elsb1 2171 elsb2 2172 eqsb1 2297 clelsb1 2298 clelsb2 2299 cbvabw 2316 clelsb1f 2340 sbabel 2363 sbralie 2744 sbcco 3007 exss 4256 inopab 4794 isarep1 5340 bezoutlemnewy 12133 |
Copyright terms: Public domain | W3C validator |