Theorem sbbii 2080

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

Syntax hints:   ↔ wb 205  [wsb 2068

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

This theorem depends on definitions:  df-bi 206  df-sb 2069

This theorem is referenced by:  2sbbii  2081  sb3an  2085  sbcom4  2093  sbievw2  2101  sbcov  2252  sbco4lem  2276  sbco4lemOLD  2277  sbco4  2278  sbex  2281  sbor  2307  sbbi  2308  sbco  2511  sbidm  2514  sbco2d  2516  sbco3  2517  sb7f  2530  sbmo  2616  cbvabv  2812  cbvabwOLD  2814  cbvab  2815  clelsb2  2867  clelsb1fw  2910  clelsb1f  2911  sbabel  2940  sbabelOLD  2941  sbralie  3395  sbccow  3734  sbcco  3737  exss  5372  inopab  5728  isarep1  6506  xpab  33579  bj-sbnf  34951  bj-sbeq  35013  bj-snsetex  35080  2uasbanh  42070  2uasbanhVD  42420  2reu8i  44492  ichv  44789  ichf  44790  ichid  44791  ichcircshi  44794  ichan  44795  ichn  44796  ichbi12i  44800  icheq  44802  ichal  44806  ichnreuop  44812  ichreuopeq  44813