Theorem sbbii 2082

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

Syntax hints:   ↔ wb 206  [wsb 2068

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069

This theorem is referenced by:  2sbbii  2083  sb3an  2087  sbcom4  2095  sbievw2  2104  cbvsbv  2106  sbco4lemOLD  2180  sbco4OLD  2181  sbcovOLD  2265  sbex  2288  sbor  2313  sbbi  2314  sbnf  2318  sbnfOLD  2319  sbco  2512  sbidm  2515  sbco2d  2517  sbco3  2518  sb7f  2530  sbmo  2615  cbvab  2809  clelsb1fw  2903  clelsb1f  2904  sbabel  2932  sbralie  3324  sbralieALT  3325  sbralieOLD  3326  sbccow  3765  sbcco  3768  exss  5418  inopab  5786  difopab  5787  xpab  35939  bj-sbeq  37146  bj-snsetex  37208  2uasbanh  44914  2uasbanhVD  45263  2reu8i  47470  ichv  47806  ichf  47807  ichid  47808  ichcircshi  47811  ichan  47812  ichn  47813  ichbi12i  47817  icheq  47819  ichal  47823  ichnreuop  47829  ichreuopeq  47830