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

Syntax hints:   ↔ wb 206  [wsb 2067

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

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

This theorem is referenced by:  2sbbii  2080  sb3an  2084  sbcom4  2092  sbievw2  2101  cbvsbv  2103  sbco4lemOLD  2177  sbco4OLD  2178  sbcovOLD  2260  sbex  2283  sbor  2308  sbbi  2309  sbnf  2313  sbnfOLD  2314  sbco  2507  sbidm  2510  sbco2d  2512  sbco3  2513  sb7f  2525  sbmo  2609  cbvab  2803  clelsb1fw  2898  clelsb1f  2899  sbabel  2927  sbralie  3318  sbralieALT  3319  sbralieOLD  3320  sbccow  3764  sbcco  3767  exss  5403  inopab  5769  difopab  5770  xpab  35768  bj-sbeq  36941  bj-snsetex  37003  2uasbanh  44600  2uasbanhVD  44949  2reu8i  47150  ichv  47486  ichf  47487  ichid  47488  ichcircshi  47491  ichan  47492  ichn  47493  ichbi12i  47497  icheq  47499  ichal  47503  ichnreuop  47509  ichreuopeq  47510