Theorem sbbii 2084

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

Syntax hints:   ↔ wb 209  [wsb 2072

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

This theorem depends on definitions:  df-bi 210  df-sb 2073

This theorem is referenced by:  2sbbii  2085  sb3an  2089  sbcom4  2097  sbievw2  2105  sbcov  2256  sbco4lem  2279  sbco4lemOLD  2280  sbco4  2281  sbex  2284  sbor  2310  sbbi  2311  sbco  2510  sbidm  2513  sbco2d  2515  sbco3  2516  sb7f  2529  sbmo  2615  cbvabv  2804  cbvabwOLD  2806  cbvab  2807  clelsb3fw  2901  clelsb3f  2902  sbabel  2931  sbralie  3371  sbccow  3706  sbcco  3709  exss  5332  inopab  5684  isarep1  6446  xpab  33346  bj-sbnf  34710  bj-sbeq  34773  bj-snsetex  34839  2uasbanh  41795  2uasbanhVD  42145  2reu8i  44220  ichv  44517  ichf  44518  ichid  44519  ichcircshi  44522  ichan  44523  ichn  44524  ichbi12i  44528  icheq  44530  ichal  44534  ichnreuop  44540  ichreuopeq  44541