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

Syntax hints:   ↔ wb 208  [wsb 2065

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

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

This theorem is referenced by:  2sbbii  2078  sb3an  2083  sbcom4  2095  sbievw2  2103  equsb3rOLD  2107  sbcov  2254  sbco4lem  2279  sbco4  2280  sbex  2284  sbanOLD  2308  sbor  2312  sbbi  2313  sbanvOLD  2322  sbbivOLD  2323  sbco  2545  sbidm  2548  sbco2d  2550  sbco3  2551  sb7f  2564  sbmo  2694  cbvabv  2889  cbvabw  2890  cbvab  2891  clelsb3vOLD  2941  clelsb3fw  2981  clelsb3f  2982  clelsb3fOLD  2983  sbabel  3015  sbralie  3471  sbccow  3794  sbcco  3797  exss  5354  inopab  5700  isarep1  6441  bj-sbnf  34164  bj-sbeq  34218  bj-snsetex  34275  wl-clelsb3df  34862  2uasbanh  40893  2uasbanhVD  41243  2reu8i  43311  ichv  43608  ichf  43609  ichid  43610  ichcircshi  43611  ichbi12i  43617  icheq  43619  ichn  43625  ichal  43626  ichan  43629  ichnreuop  43633  ichreuopeq  43634