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  3404  sbccow  3739  sbcco  3742  exss  5377  inopab  5733  isarep1  6515  xpab  33663  bj-sbnf  35010  bj-sbeq  35072  bj-snsetex  35139  2uasbanh  42140  2uasbanhVD  42490  2reu8i  44561  ichv  44857  ichf  44858  ichid  44859  ichcircshi  44862  ichan  44863  ichn  44864  ichbi12i  44868  icheq  44870  ichal  44874  ichnreuop  44880  ichreuopeq  44881