Theorem sbbii 2079

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

Syntax hints:   ↔ wb 205  [wsb 2067

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

This theorem depends on definitions:  df-bi 206  df-sb 2068

This theorem is referenced by:  2sbbii  2080  sb3an  2084  sbcom4  2092  sbievw2  2099  sbcov  2248  sbco4lem  2272  sbco4lemOLD  2273  sbco4  2274  sbex  2277  sbor  2303  sbbi  2304  cbvsbv  2359  sbco  2506  sbidm  2509  sbco2d  2511  sbco3  2512  sb7f  2524  sbmo  2610  cbvabwOLD  2807  cbvab  2808  clelsb2OLD  2862  clelsb1fw  2907  clelsb1f  2908  sbabel  2938  sbabelOLD  2939  sbralie  3354  sbralieALT  3355  sbccow  3800  sbcco  3803  exss  5463  inopab  5829  difopab  5830  isarep1OLD  6638  xpab  34690  bj-sbnf  35714  bj-sbeq  35776  bj-snsetex  35839  2uasbanh  43312  2uasbanhVD  43662  2reu8i  45811  ichv  46107  ichf  46108  ichid  46109  ichcircshi  46112  ichan  46113  ichn  46114  ichbi12i  46118  icheq  46120  ichal  46124  ichnreuop  46130  ichreuopeq  46131