New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE 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 | ⊢ ([y / x]φ ↔ [y / x]ψ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sbbii.1 | . . . 4 ⊢ (φ ↔ ψ) | |
2 | 1 | biimpi 186 | . . 3 ⊢ (φ → ψ) |
3 | 2 | sbimi 1652 | . 2 ⊢ ([y / x]φ → [y / x]ψ) |
4 | 1 | biimpri 197 | . . 3 ⊢ (ψ → φ) |
5 | 4 | sbimi 1652 | . 2 ⊢ ([y / x]ψ → [y / x]φ) |
6 | 3, 5 | impbii 180 | 1 ⊢ ([y / x]φ ↔ [y / x]ψ) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 176 [wsb 1648 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1546 ax-5 1557 |
This theorem depends on definitions: df-bi 177 df-an 360 df-ex 1542 df-sb 1649 |
This theorem is referenced by: sbn 2062 sbor 2066 sban 2069 sb3an 2070 sbbi 2071 sbco2d 2087 sbco3 2088 equsb3 2102 elsb3 2103 elsb4 2104 dfsb7 2119 sb7f 2120 sbex 2128 sbmo 2234 2eu6 2289 eqsb3 2454 clelsb3 2455 sbabel 2515 sbralie 2848 sbcco 3068 |
Copyright terms: Public domain | W3C validator |