Theorem sbbii 2081

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

Syntax hints:   ↔ wb 206  [wsb 2067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068

This theorem is referenced by:  2sbbii  2082  sb3an  2086  sbcom4  2094  sbievw2  2103  cbvsbv  2105  sbco4lemOLD  2179  sbco4OLD  2180  sbcovOLD  2262  sbex  2285  sbor  2310  sbbi  2311  sbnf  2315  sbnfOLD  2316  sbco  2509  sbidm  2512  sbco2d  2514  sbco3  2515  sb7f  2527  sbmo  2611  cbvab  2805  clelsb1fw  2899  clelsb1f  2900  sbabel  2928  sbralie  3319  sbralieALT  3320  sbralieOLD  3321  sbccow  3760  sbcco  3763  exss  5406  inopab  5773  difopab  5774  xpab  35791  bj-sbeq  36966  bj-snsetex  37028  2uasbanh  44679  2uasbanhVD  45028  2reu8i  47238  ichv  47574  ichf  47575  ichid  47576  ichcircshi  47579  ichan  47580  ichn  47581  ichbi12i  47585  icheq  47587  ichal  47591  ichnreuop  47597  ichreuopeq  47598