Theorem sbbii 2076

Description: Infer substitution into both sides of a logical equivalence. (Contributed by NM, 14-May-1993.)

Hypothesis

Ref	Expression
sbbii.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
sbbii	⊢ ([𝑡 / 𝑥]𝜑 ↔ [𝑡 / 𝑥]𝜓)

Proof of Theorem 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 ⊢ ([𝑡 / 𝑥]𝜑 ↔ [𝑡 / 𝑥]𝜓)

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 1793  ax-4 1807

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  2175  sbco4OLD  2176  sbcovOLD  2258  sbco4lemOLDOLD  2282  sbex  2285  sbor  2311  sbbi  2312  sbnf  2316  sbnfOLD  2317  sbco  2515  sbidm  2518  sbco2d  2520  sbco3  2521  sb7f  2533  sbmo  2617  cbvab  2817  clelsb2OLD  2873  clelsb1fw  2912  clelsb1f  2913  sbabel  2944  sbabelOLD  2945  sbralie  3366  sbralieALT  3367  sbccow  3827  sbcco  3830  exss  5483  inopab  5853  difopab  5854  isarep1OLD  6668  xpab  35688  bj-sbeq  36867  bj-snsetex  36929  2uasbanh  44532  2uasbanhVD  44882  2reu8i  47028  ichv  47323  ichf  47324  ichid  47325  ichcircshi  47328  ichan  47329  ichn  47330  ichbi12i  47334  icheq  47336  ichal  47340  ichnreuop  47346  ichreuopeq  47347