Theorem sbbii 2108

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 218	. . 3 ⊢ (𝜑 → 𝜓)
3	2	sbimi 2106	. 2 ⊢ ([𝑡 / 𝑥]𝜑 → [𝑡 / 𝑥]𝜓)
4	1	biimpri 230	. . 3 ⊢ (𝜓 → 𝜑)
5	4	sbimi 2106	. 2 ⊢ ([𝑡 / 𝑥]𝜓 → [𝑡 / 𝑥]𝜑)
6	3, 5	impbii 211	1 ⊢ ([𝑡 / 𝑥]𝜑 ↔ [𝑡 / 𝑥]𝜓)

Syntax hints:   ↔ wb 208  [wsb 2089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828

This theorem depends on definitions:  df-bi 209  df-an 400  df-sb 2090

This theorem is referenced by:  2sbbii  2109  sb3an  2113  sbcom4  2121  sbievw2  2131  cbvsbv  2133  sbco4lemOLD  2206  sbco4OLD  2207  sbcovOLD  2291  sbex  2314  sbor  2339  sbbi  2340  sbnf  2344  sbco  2537  sbidm  2540  sbco2d  2542  sbco3  2543  sb7f  2555  sbmo  2640  cbvab  2833  clelsb1fw  2927  clelsb1f  2928  sbabel  2955  sbralie  3339  sbralieALT  3340  sbralieOLD  3341  sbccow  3767  sbcco  3770  exss  5429  inopab  5800  difopab  5801  xpab  36040  bj-sbeq  37350  bj-snsetex  37412  2uasbanh  45101  2uasbanhVD  45450  2reu8i  47671  ichv  48019  ichf  48020  ichid  48021  ichcircshi  48024  ichan  48025  ichn  48026  ichbi12i  48030  icheq  48032  ichal  48036  ichnreuop  48042  ichreuopeq  48043