Theorem sbbii 2079

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 215	. . 3 ⊢ (𝜑 → 𝜓)
3	2	sbimi 2077	. 2 ⊢ ([𝑡 / 𝑥]𝜑 → [𝑡 / 𝑥]𝜓)
4	1	biimpri 227	. . 3 ⊢ (𝜓 → 𝜑)
5	4	sbimi 2077	. 2 ⊢ ([𝑡 / 𝑥]𝜓 → [𝑡 / 𝑥]𝜑)
6	3, 5	impbii 208	1 ⊢ ([𝑡 / 𝑥]𝜑 ↔ [𝑡 / 𝑥]𝜓)

Syntax hints:   ↔ wb 205  [wsb 2067

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

This theorem depends on definitions:  df-bi 206  df-sb 2068

This theorem is referenced by:  2sbbii  2080  sb3an  2084  sbcom4  2092  sbievw2  2099  sbcov  2248  sbco4lem  2272  sbco4lemOLD  2273  sbco4  2274  sbex  2277  sbor  2303  sbbi  2304  cbvsbv  2359  sbco  2506  sbidm  2509  sbco2d  2511  sbco3  2512  sb7f  2524  sbmo  2610  cbvabwOLD  2807  cbvab  2808  clelsb2OLD  2862  clelsb1fw  2907  clelsb1f  2908  sbabel  2938  sbabelOLD  2939  sbralie  3354  sbralieALT  3355  sbccow  3800  sbcco  3803  exss  5463  inopab  5829  difopab  5830  isarep1OLD  6638  xpab  34987  bj-sbnf  36022  bj-sbeq  36084  bj-snsetex  36147  2uasbanh  43624  2uasbanhVD  43974  2reu8i  46120  ichv  46416  ichf  46417  ichid  46418  ichcircshi  46421  ichan  46422  ichn  46423  ichbi12i  46427  icheq  46429  ichal  46433  ichnreuop  46439  ichreuopeq  46440