Theorem sbbii 2110

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 219	. . 3 ⊢ (𝜑 → 𝜓)
3	2	sbimi 2108	. 2 ⊢ ([𝑡 / 𝑥]𝜑 → [𝑡 / 𝑥]𝜓)
4	1	biimpri 231	. . 3 ⊢ (𝜓 → 𝜑)
5	4	sbimi 2108	. 2 ⊢ ([𝑡 / 𝑥]𝜓 → [𝑡 / 𝑥]𝜑)
6	3, 5	impbii 212	1 ⊢ ([𝑡 / 𝑥]𝜑 ↔ [𝑡 / 𝑥]𝜓)

Syntax hints:   ↔ wb 209  [wsb 2096

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097

This theorem is referenced by:  2sbbii  2111  sb3an  2115  sbcom4  2123  sbievw2  2133  cbvsbv  2135  sbco4lemOLD  2208  sbco4OLD  2209  sbcovOLD  2293  sbex  2316  sbor  2341  sbbi  2342  sbnf  2346  sbco  2539  sbidm  2542  sbco2d  2544  sbco3  2545  sb7f  2557  sbmo  2642  cbvab  2835  clelsb1fw  2929  clelsb1f  2930  sbabel  2957  sbralie  3342  sbralieALT  3343  sbralieOLD  3344  sbccow  3768  sbcco  3771  exss  5446  inopab  5818  difopab  5819  xpab  36196  bj-sbeq  37514  bj-snsetex  37577  2uasbanh  45250  2uasbanhVD  45599  2reu8i  47827  ichv  48175  ichf  48176  ichid  48177  ichcircshi  48180  ichan  48181  ichn  48182  ichbi12i  48186  icheq  48188  ichal  48192  ichnreuop  48198  ichreuopeq  48199