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 119 | . . 3 ⊢ (𝜑 → 𝜓) |
3 | 2 | sbimi 1722 | . 2 ⊢ ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓) |
4 | 1 | biimpri 132 | . . 3 ⊢ (𝜓 → 𝜑) |
5 | 4 | sbimi 1722 | . 2 ⊢ ([𝑦 / 𝑥]𝜓 → [𝑦 / 𝑥]𝜑) |
6 | 3, 5 | impbii 125 | 1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜓) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 [wsb 1720 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1408 ax-gen 1410 ax-ie1 1454 ax-ie2 1455 ax-4 1472 ax-ial 1499 |
This theorem depends on definitions: df-bi 116 df-sb 1721 |
This theorem is referenced by: sbco2v 1898 equsb3 1902 sbn 1903 sbim 1904 sbor 1905 sban 1906 sb3an 1909 sbbi 1910 sbco2h 1915 sbco2d 1917 sbco2vd 1918 sbco3v 1920 sbco3 1925 elsb3 1929 elsb4 1930 sbcom2v2 1939 sbcom2 1940 dfsb7 1944 sb7f 1945 sb7af 1946 sbal 1953 sbal1 1955 sbex 1957 sbco4lem 1959 sbco4 1960 sbmo 2036 eqsb3 2221 clelsb3 2222 clelsb4 2223 clelsb3f 2262 sbabel 2284 sbralie 2644 sbcco 2903 exss 4119 inopab 4641 isarep1 5179 bezoutlemnewy 11611 |
Copyright terms: Public domain | W3C validator |