Theorem sbbii 2076

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

Syntax hints:   ↔ wb 206  [wsb 2064

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

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

This theorem is referenced by:  2sbbii  2077  sb3an  2081  sbcom4  2089  sbievw2  2098  cbvsbv  2100  sbco4lemOLD  2174  sbco4OLD  2175  sbcovOLD  2257  sbex  2281  sbor  2307  sbbi  2308  sbnf  2312  sbnfOLD  2313  sbco  2511  sbidm  2514  sbco2d  2516  sbco3  2517  sb7f  2529  sbmo  2613  cbvab  2807  clelsb2OLD  2863  clelsb1fw  2902  clelsb1f  2903  sbabel  2931  sbralie  3337  sbralieALT  3338  sbccow  3788  sbcco  3791  exss  5438  inopab  5808  difopab  5809  isarep1OLD  6627  xpab  35743  bj-sbeq  36919  bj-snsetex  36981  2uasbanh  44586  2uasbanhVD  44935  2reu8i  47142  ichv  47463  ichf  47464  ichid  47465  ichcircshi  47468  ichan  47469  ichn  47470  ichbi12i  47474  icheq  47476  ichal  47480  ichnreuop  47486  ichreuopeq  47487