Theorem sbbii 2081

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

Syntax hints:   ↔ wb 208  [wsb 2069

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

This theorem depends on definitions:  df-bi 209  df-sb 2070

This theorem is referenced by:  2sbbii  2082  sb3an  2087  sbcom4  2099  sbievw2  2107  equsb3rOLD  2111  sbcov  2258  sbco4lem  2283  sbco4  2284  sbex  2288  sbanOLD  2312  sbor  2316  sbbi  2317  sbanvOLD  2326  sbbivOLD  2327  sbco  2549  sbidm  2552  sbco2d  2554  sbco3  2555  sb7f  2568  sbmo  2698  cbvabv  2889  cbvabw  2890  cbvab  2891  clelsb3vOLD  2941  clelsb3fw  2981  clelsb3f  2982  clelsb3fOLD  2983  sbabel  3015  sbralie  3463  sbccow  3786  sbcco  3789  exss  5341  inopab  5687  isarep1  6428  bj-sbnf  34171  bj-sbeq  34234  bj-snsetex  34291  wl-clelsb3df  34897  2uasbanh  40985  2uasbanhVD  41335  2reu8i  43402  ichv  43699  ichf  43700  ichid  43701  ichcircshi  43702  ichbi12i  43705  icheq  43707  ichn  43711  ichal  43712  ichan  43715  ichnreuop  43719  ichreuopeq  43720