Theorem sbbii 1789

Description: Infer substitution into both sides of a logical equivalence. (Contributed by NM, 5-Aug-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 120	. . 3 ⊢ (𝜑 → 𝜓)
3	2	sbimi 1788	. 2 ⊢ ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓)
4	1	biimpri 133	. . 3 ⊢ (𝜓 → 𝜑)
5	4	sbimi 1788	. 2 ⊢ ([𝑦 / 𝑥]𝜓 → [𝑦 / 𝑥]𝜑)
6	3, 5	impbii 126	1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜓)

Syntax hints:   ↔ wb 105  [wsb 1786

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-ial 1558

This theorem depends on definitions:  df-bi 117  df-sb 1787

This theorem is referenced by:  sbco2vh  1974  equsb3  1980  sbn  1981  sbim  1982  sbor  1983  sban  1984  sb3an  1987  sbbi  1988  sbco2h  1993  sbco2d  1995  sbco2vd  1996  sbco3v  1998  sbco3  2003  sbcom2v2  2015  sbcom2  2016  dfsb7  2020  sb7f  2021  sb7af  2022  sbal  2029  sbal1  2031  sbex  2033  sbco4lem  2035  sbco4  2036  sbmo  2114  elsb1  2184  elsb2  2185  eqsb1  2310  clelsb1  2311  clelsb2  2312  cbvabw  2329  clelsb1f  2353  sbabel  2376  sbralie  2757  sbcco  3022  exss  4276  inopab  4815  isarep1  5366  bezoutlemnewy  12367