Theorem sbbii 1873

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 204	. . 3 ⊢ (𝜑 → 𝜓)
3	2	sbimi 1872	. 2 ⊢ ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓)
4	1	biimpri 216	. . 3 ⊢ (𝜓 → 𝜑)
5	4	sbimi 1872	. 2 ⊢ ([𝑦 / 𝑥]𝜓 → [𝑦 / 𝑥]𝜑)
6	3, 5	impbii 197	1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜓)

Syntax hints:   ↔ wb 194  [wsb 1866

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

This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695  df-sb 1867

This theorem is referenced by:  sbor  2385  sban  2386  sb3an  2387  sbbi  2388  sbco  2399  sbidm  2401  sbco2d  2403  sbco3  2404  equsb3  2419  equsb3ALT  2420  elsb3  2421  elsb4  2422  sbcom4  2433  sb7f  2440  sbex  2450  sbco4lem  2452  sbco4  2453  sbmo  2502  eqsb3  2714  clelsb3  2715  cbvab  2732  sbabel  2778  sbralie  3159  sbcco  3424  exss  4852  inopab  5162  isarep1  5877  clelsb3f  28510  bj-sbnf  31822  bj-clelsb3  31838  bj-sbeq  31884  bj-snsetex  31940  2uasbanh  37594  2uasbanhVD  37965