Theorem sbbii 2112

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

This proof depends on syntax axioms:   ↔ wb 209  [wsb 2098

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099

This theorem is used by:  2sbbii  2113  sb3an  2117  sbcom4  2125  sbievw2  2134  cbvsbv  2136  sbex  2314  sbor  2339  sbbi  2340  sbnf  2344  sbco  2536  sbidm  2539  sbco2d  2541  sbco3  2542  sb7f  2554  sbmo  2639  cbvab  2832  clelsb1fw  2926  clelsb1f  2927  sbabel  2954  sbralie  3338  sbralieALT  3339  sbralieOLD  3340  sbccow  3761  sbcco  3764  exss  5430  inopab  5806  difopab  5807  xpab  36583  bj-sbeq  37905  bj-snsetex  37968  2uasbanh  45637  2uasbanhVD  45986  2reu8i  48276  ichv  48624  ichf  48625  ichid  48626  ichcircshi  48629  ichan  48630  ichn  48631  ichbi12i  48635  icheq  48637  ichal  48641  ichnreuop  48647  ichreuopeq  48648