Theorem sbbii 2081

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

Syntax hints:   ↔ wb 206  [wsb 2067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068

This theorem is referenced by:  2sbbii  2082  sb3an  2086  sbcom4  2094  sbievw2  2103  cbvsbv  2105  sbco4lemOLD  2179  sbco4OLD  2180  sbcovOLD  2264  sbex  2287  sbor  2312  sbbi  2313  sbnf  2317  sbnfOLD  2318  sbco  2511  sbidm  2514  sbco2d  2516  sbco3  2517  sb7f  2529  sbmo  2614  cbvab  2808  clelsb1fw  2902  clelsb1f  2903  sbabel  2931  sbralie  3322  sbralieALT  3323  sbralieOLD  3324  sbccow  3763  sbcco  3766  exss  5411  inopab  5778  difopab  5779  xpab  35920  bj-sbeq  37102  bj-snsetex  37164  2uasbanh  44798  2uasbanhVD  45147  2reu8i  47355  ichv  47691  ichf  47692  ichid  47693  ichcircshi  47696  ichan  47697  ichn  47698  ichbi12i  47702  icheq  47704  ichal  47708  ichnreuop  47714  ichreuopeq  47715