Theorem sbbii 2112

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

Syntax hints:   ↔ wb 209  [wsb 2093

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-sb 2094

This theorem is referenced by:  2sbbii  2113  sb3an  2117  sbcom4  2125  sbievw2  2135  cbvsbv  2137  sbco4lemOLD  2210  sbco4OLD  2211  sbcovOLD  2295  sbex  2318  sbor  2343  sbbi  2344  sbnf  2348  sbco  2541  sbidm  2544  sbco2d  2546  sbco3  2547  sb7f  2559  sbmo  2644  cbvab  2837  clelsb1fw  2931  clelsb1f  2932  sbabel  2959  sbralie  3343  sbralieALT  3344  sbralieOLD  3345  sbccow  3770  sbcco  3773  exss  5435  inopab  5807  difopab  5808  xpab  36089  bj-sbeq  37398  bj-snsetex  37460  2uasbanh  45135  2uasbanhVD  45484  2reu8i  47705  ichv  48053  ichf  48054  ichid  48055  ichcircshi  48058  ichan  48059  ichn  48060  ichbi12i  48064  icheq  48066  ichal  48070  ichnreuop  48076  ichreuopeq  48077