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  2136  cbvsbv  2138  sbco4lemOLD  2211  sbco4OLD  2212  sbcovOLD  2296  sbex  2319  sbor  2344  sbbi  2345  sbnf  2349  sbco  2542  sbidm  2545  sbco2d  2547  sbco3  2548  sb7f  2560  sbmo  2645  cbvab  2838  clelsb1fw  2932  clelsb1f  2933  sbabel  2960  sbralie  3345  sbralieALT  3346  sbralieOLD  3347  sbccow  3770  sbcco  3773  exss  5449  inopab  5821  difopab  5822  xpab  36239  bj-sbeq  37577  bj-snsetex  37640  2uasbanh  45311  2uasbanhVD  45660  2reu8i  47891  ichv  48239  ichf  48240  ichid  48241  ichcircshi  48244  ichan  48245  ichn  48246  ichbi12i  48250  icheq  48252  ichal  48256  ichnreuop  48262  ichreuopeq  48263