Theorem sbbii 2077

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

Syntax hints:   ↔ wb 206  [wsb 2065

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 2066

This theorem is referenced by:  2sbbii  2078  sb3an  2082  sbcom4  2090  sbievw2  2099  cbvsbv  2101  sbco4lemOLD  2175  sbco4OLD  2176  sbcovOLD  2258  sbex  2281  sbor  2306  sbbi  2307  sbnf  2311  sbnfOLD  2312  sbco  2505  sbidm  2508  sbco2d  2510  sbco3  2511  sb7f  2523  sbmo  2607  cbvab  2801  clelsb1fw  2895  clelsb1f  2896  sbabel  2924  sbralie  3326  sbralieALT  3327  sbralieOLD  3328  sbccow  3776  sbcco  3779  exss  5423  inopab  5792  difopab  5793  isarep1OLD  6607  xpab  35713  bj-sbeq  36889  bj-snsetex  36951  2uasbanh  44551  2uasbanhVD  44900  2reu8i  47111  ichv  47447  ichf  47448  ichid  47449  ichcircshi  47452  ichan  47453  ichn  47454  ichbi12i  47458  icheq  47460  ichal  47464  ichnreuop  47470  ichreuopeq  47471