Theorem sbbii 2073

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

Syntax hints:   ↔ wb 206  [wsb 2061

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

This theorem depends on definitions:  df-bi 207  df-sb 2062

This theorem is referenced by:  2sbbii  2074  sb3an  2078  sbcom4  2086  sbievw2  2095  cbvsbv  2097  sbco4lemOLD  2171  sbco4OLD  2172  sbcovOLD  2254  sbco4lemOLDOLD  2276  sbex  2279  sbor  2305  sbbi  2306  sbnf  2310  sbnfOLD  2311  sbco  2509  sbidm  2512  sbco2d  2514  sbco3  2515  sb7f  2527  sbmo  2611  cbvab  2811  clelsb2OLD  2867  clelsb1fw  2906  clelsb1f  2907  sbabel  2935  sbabelOLD  2936  sbralie  3355  sbralieALT  3356  sbccow  3813  sbcco  3816  exss  5473  inopab  5841  difopab  5842  isarep1OLD  6657  xpab  35705  bj-sbeq  36883  bj-snsetex  36945  2uasbanh  44558  2uasbanhVD  44908  2reu8i  47062  ichv  47373  ichf  47374  ichid  47375  ichcircshi  47378  ichan  47379  ichn  47380  ichbi12i  47384  icheq  47386  ichal  47390  ichnreuop  47396  ichreuopeq  47397