Theorem sbbii 2076

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

Syntax hints:   ↔ wb 206  [wsb 2064

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 2065

This theorem is referenced by:  2sbbii  2077  sb3an  2081  sbcom4  2089  sbievw2  2098  cbvsbv  2100  sbco4lemOLD  2174  sbco4OLD  2175  sbcovOLD  2257  sbex  2281  sbor  2307  sbbi  2308  sbnf  2312  sbnfOLD  2313  sbco  2512  sbidm  2515  sbco2d  2517  sbco3  2518  sb7f  2530  sbmo  2614  cbvab  2814  clelsb2OLD  2870  clelsb1fw  2909  clelsb1f  2910  sbabel  2938  sbabelOLD  2939  sbralie  3358  sbralieALT  3359  sbccow  3811  sbcco  3814  exss  5468  inopab  5839  difopab  5840  isarep1OLD  6657  xpab  35726  bj-sbeq  36902  bj-snsetex  36964  2uasbanh  44581  2uasbanhVD  44931  2reu8i  47125  ichv  47436  ichf  47437  ichid  47438  ichcircshi  47441  ichan  47442  ichn  47443  ichbi12i  47447  icheq  47449  ichal  47453  ichnreuop  47459  ichreuopeq  47460