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  sbco4lemOLD  2210  sbco4OLD  2211  sbex  2316  sbor  2341  sbbi  2342  sbnf  2346  sbco  2538  sbidm  2541  sbco2d  2543  sbco3  2544  sb7f  2556  sbmo  2641  cbvab  2834  clelsb1fw  2928  clelsb1f  2929  sbabel  2956  sbralie  3340  sbralieALT  3341  sbralieOLD  3342  sbccow  3765  sbcco  3768  exss  5442  inopab  5814  difopab  5815  xpab  36313  bj-sbeq  37652  bj-snsetex  37715  2uasbanh  45392  2uasbanhVD  45741  2reu8i  48009  ichv  48357  ichf  48358  ichid  48359  ichcircshi  48362  ichan  48363  ichn  48364  ichbi12i  48368  icheq  48370  ichal  48374  ichnreuop  48380  ichreuopeq  48381