Theorem sbbii 1695

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 118	. . 3 ⊢ (𝜑 → 𝜓)
3	2	sbimi 1694	. 2 ⊢ ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓)
4	1	biimpri 131	. . 3 ⊢ (𝜓 → 𝜑)
5	4	sbimi 1694	. 2 ⊢ ([𝑦 / 𝑥]𝜓 → [𝑦 / 𝑥]𝜑)
6	3, 5	impbii 124	1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜓)

Syntax hints:   ↔ wb 103  [wsb 1692

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445  ax-ial 1472

This theorem depends on definitions:  df-bi 115  df-sb 1693

This theorem is referenced by:  sbco2v  1869  equsb3  1873  sbn  1874  sbim  1875  sbor  1876  sban  1877  sb3an  1880  sbbi  1881  sbco2h  1886  sbco2d  1888  sbco2vd  1889  sbco3v  1891  sbco3  1896  elsb3  1900  elsb4  1901  sbcom2v2  1910  sbcom2  1911  dfsb7  1915  sb7f  1916  sb7af  1917  sbal  1924  sbal1  1926  sbex  1928  sbco4lem  1930  sbco4  1931  sbmo  2007  eqsb3  2191  clelsb3  2192  clelsb4  2193  clelsb3f  2232  sbabel  2254  sbralie  2603  sbcco  2861  exss  4054  inopab  4568  isarep1  5100  bezoutlemnewy  11259