Theorem sbbii 2116

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

Syntax hints:   ↔ wb 209  [wsb 2097

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-sb 2098

This theorem is referenced by:  2sbbii  2117  sb3an  2121  sbcom4  2129  sbievw2  2139  cbvsbv  2141  sbco4lemOLD  2214  sbco4OLD  2215  sbcovOLD  2299  sbex  2322  sbor  2347  sbbi  2348  sbnf  2352  sbco  2545  sbidm  2548  sbco2d  2550  sbco3  2551  sb7f  2563  sbmo  2648  cbvab  2841  clelsb1fw  2935  clelsb1f  2936  sbabel  2963  sbralie  3349  sbralieALT  3350  sbralieOLD  3351  sbccow  3776  sbcco  3779  exss  5447  inopab  5819  difopab  5820  xpab  36153  bj-sbeq  37461  bj-snsetex  37524  2uasbanh  45199  2uasbanhVD  45548  2reu8i  47776  ichv  48124  ichf  48125  ichid  48126  ichcircshi  48129  ichan  48130  ichn  48131  ichbi12i  48135  icheq  48137  ichal  48141  ichnreuop  48147  ichreuopeq  48148