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 1798  ax-4 1812

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  2249  sbco4lem  2273  sbco4lemOLD  2274  sbco4  2275  sbex  2278  sbor  2304  sbbi  2305  sbco  2511  sbidm  2514  sbco2d  2516  sbco3  2517  sb7f  2530  sbmo  2616  cbvabv  2811  cbvabwOLD  2813  cbvab  2814  clelsb2OLD  2868  clelsb1fw  2911  clelsb1f  2912  sbabel  2941  sbabelOLD  2942  sbralie  3406  sbccow  3739  sbcco  3742  exss  5378  inopab  5739  isarep1  6522  xpab  33677  bj-sbnf  35024  bj-sbeq  35086  bj-snsetex  35153  2uasbanh  42181  2uasbanhVD  42531  2reu8i  44605  ichv  44901  ichf  44902  ichid  44903  ichcircshi  44906  ichan  44907  ichn  44908  ichbi12i  44912  icheq  44914  ichal  44918  ichnreuop  44924  ichreuopeq  44925