Theorem sbbii 2113

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100

This theorem is used by:  2sbbii  2114  sb3an  2118  sbcom4  2126  sbievw2  2135  cbvsbv  2137  sbex  2315  sbor  2340  sbbi  2341  sbnf  2345  sbco  2537  sbidm  2540  sbco2d  2542  sbco3  2543  sb7f  2555  sbmo  2640  cbvab  2833  clelsb1fw  2927  clelsb1f  2928  sbabel  2955  sbralie  3339  sbralieALT  3340  sbralieOLD  3341  sbccow  3762  sbcco  3765  exss  5431  inopab  5807  difopab  5808  xpab  36460  bj-sbeq  37783  bj-snsetex  37846  2uasbanh  45503  2uasbanhVD  45852  2reu8i  48127  ichv  48475  ichf  48476  ichid  48477  ichcircshi  48480  ichan  48481  ichn  48482  ichbi12i  48486  icheq  48488  ichal  48492  ichnreuop  48498  ichreuopeq  48499