Theorem sbbii 2052

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

Syntax hints:   ↔ wb 207  [wsb 2040

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789

This theorem depends on definitions:  df-bi 208  df-sb 2041

This theorem is referenced by:  2sbbii  2053  sb3an  2058  sbcom4  2068  sbievw2  2072  equsb3rOLD  2076  sbcov  2219  sbco4lem  2247  sbco4  2248  sbex  2252  sbanOLD  2276  sbor  2279  sbbi  2280  sbanvOLD  2289  sbbivOLD  2290  sbco  2501  sbidm  2504  sbco2d  2506  sbco3  2507  sb7f  2519  sbmo  2664  clelsb3vOLD  2909  cbvabv  2925  cbvab  2926  clelsb3f  2951  clelsb3fOLD  2952  sbabel  2981  sbralie  3414  sbcco  3724  exss  5240  inopab  5579  isarep1  6304  bj-sbnf  33678  bj-sbeq  33733  bj-snsetex  33826  wl-clelsb3df  34340  2uasbanh  40386  2uasbanhVD  40736  2reu8i  42782  ichv  43045  ichf  43046  ichid  43047  ichcircshi  43048  ichbi12i  43054  icheq  43056  ichn  43062  ichal  43063  ichan  43066  ichnreuop  43070  ichreuopeq  43071