Theorem sbbii 2082

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

Syntax hints:   ↔ wb 206  [wsb 2068

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069

This theorem is referenced by:  2sbbii  2083  sb3an  2087  sbcom4  2095  sbievw2  2104  cbvsbv  2106  sbco4lemOLD  2180  sbco4OLD  2181  sbcovOLD  2265  sbex  2288  sbor  2313  sbbi  2314  sbnf  2318  sbnfOLD  2319  sbco  2512  sbidm  2515  sbco2d  2517  sbco3  2518  sb7f  2530  sbmo  2615  cbvab  2809  clelsb1fw  2903  clelsb1f  2904  sbabel  2932  sbralie  3316  sbralieALT  3317  sbralieOLD  3318  sbccow  3752  sbcco  3755  exss  5410  inopab  5778  difopab  5779  xpab  35924  bj-sbeq  37224  bj-snsetex  37286  2uasbanh  45006  2uasbanhVD  45355  2reu8i  47573  ichv  47921  ichf  47922  ichid  47923  ichcircshi  47926  ichan  47927  ichn  47928  ichbi12i  47932  icheq  47934  ichal  47938  ichnreuop  47944  ichreuopeq  47945