Theorem sbbii 2077

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

Syntax hints:   ↔ wb 206  [wsb 2065

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

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

This theorem is referenced by:  2sbbii  2078  sb3an  2082  sbcom4  2090  sbievw2  2099  cbvsbv  2101  sbco4lemOLD  2175  sbco4OLD  2176  sbcovOLD  2258  sbex  2281  sbor  2306  sbbi  2307  sbnf  2311  sbnfOLD  2312  sbco  2505  sbidm  2508  sbco2d  2510  sbco3  2511  sb7f  2523  sbmo  2607  cbvab  2801  clelsb1fw  2895  clelsb1f  2896  sbabel  2924  sbralie  3317  sbralieALT  3318  sbralieOLD  3319  sbccow  3767  sbcco  3770  exss  5410  inopab  5776  difopab  5777  xpab  35701  bj-sbeq  36877  bj-snsetex  36939  2uasbanh  44538  2uasbanhVD  44887  2reu8i  47101  ichv  47437  ichf  47438  ichid  47439  ichcircshi  47442  ichan  47443  ichn  47444  ichbi12i  47448  icheq  47450  ichal  47454  ichnreuop  47460  ichreuopeq  47461