Theorem sbbii 2087

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

Syntax hints:   ↔ wb 207  [wsb 2073

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074

This theorem is referenced by:  2sbbii  2088  sb3an  2092  sbcom4  2100  sbievw2  2109  cbvsbv  2111  sbco4lemOLD  2184  sbco4OLD  2185  sbcovOLD  2269  sbex  2292  sbor  2317  sbbi  2318  sbnf  2322  sbco  2515  sbidm  2518  sbco2d  2520  sbco3  2521  sb7f  2533  sbmo  2618  cbvab  2812  clelsb1fw  2906  clelsb1f  2907  sbabel  2934  sbralie  3318  sbralieALT  3319  sbralieOLD  3320  sbccow  3753  sbcco  3756  exss  5409  inopab  5779  difopab  5780  xpab  35961  bj-sbeq  37261  bj-snsetex  37323  2uasbanh  45012  2uasbanhVD  45361  2reu8i  47583  ichv  47931  ichf  47932  ichid  47933  ichcircshi  47936  ichan  47937  ichn  47938  ichbi12i  47942  icheq  47944  ichal  47948  ichnreuop  47954  ichreuopeq  47955