Theorem sbbii 2082

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

Syntax hints:   ↔ wb 206  [wsb 2068

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069

This theorem is referenced by:  2sbbii  2083  sb3an  2087  sbcom4  2095  sbievw2  2104  cbvsbv  2106  sbco4lemOLD  2180  sbco4OLD  2181  sbcovOLD  2265  sbex  2288  sbor  2313  sbbi  2314  sbnf  2318  sbco  2511  sbidm  2514  sbco2d  2516  sbco3  2517  sb7f  2529  sbmo  2614  cbvab  2808  clelsb1fw  2902  clelsb1f  2903  sbabel  2931  sbralie  3315  sbralieALT  3316  sbralieOLD  3317  sbccow  3751  sbcco  3754  exss  5415  inopab  5785  difopab  5786  xpab  35908  bj-sbeq  37208  bj-snsetex  37270  2uasbanh  44988  2uasbanhVD  45337  2reu8i  47561  ichv  47909  ichf  47910  ichid  47911  ichcircshi  47914  ichan  47915  ichn  47916  ichbi12i  47920  icheq  47922  ichal  47926  ichnreuop  47932  ichreuopeq  47933