Theorem sbbii 2115

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

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

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 1945  ax-6 2002  ax-7 2043

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

This theorem is used by:  2sbbii  2116  sb3an  2120  sbcom4  2128  sbievw2  2137  cbvsbv  2139  sbex  2318  sbor  2343  sbbi  2344  sbnf  2348  sbco  2539  sbidm  2542  sbco2d  2544  sbco3  2545  sb7f  2557  sbmo  2642  cbvab  2836  clelsb1fw  2930  clelsb1f  2931  sbabel  2958  sbralie  3342  sbralieALT  3343  sbralieOLD  3344  sbccow  3765  sbcco  3768  exss  5436  inopab  5814  difopab  5815  xpab  36682  bj-sbeq  38004  bj-snsetex  38067  2uasbanh  45746  2uasbanhVD  46095  2reu8i  48399  ichv  48746  ichf  48747  ichid  48748  ichcircshi  48751  ichan  48752  ichn  48753  ichbi12i  48757  icheq  48759  ichal  48763  ichnreuop  48769  ichreuopeq  48770