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  2506  sbidm  2509  sbco2d  2511  sbco3  2512  sb7f  2524  sbmo  2608  cbvab  2802  clelsb1fw  2896  clelsb1f  2897  sbabel  2925  sbralie  3328  sbralieALT  3329  sbralieOLD  3330  sbccow  3779  sbcco  3782  exss  5426  inopab  5795  difopab  5796  isarep1OLD  6610  xpab  35720  bj-sbeq  36896  bj-snsetex  36958  2uasbanh  44558  2uasbanhVD  44907  2reu8i  47118  ichv  47454  ichf  47455  ichid  47456  ichcircshi  47459  ichan  47460  ichn  47461  ichbi12i  47465  icheq  47467  ichal  47471  ichnreuop  47477  ichreuopeq  47478