Theorem bisb 855

Description: Infer substitution into both sides of a logical equivalence.

Hypothesis

Ref	Expression
bisb.1	⊢ (φ ↔ ψ)

Assertion

Ref	Expression
bisb	⊢ ([y / x]φ ↔ [y / x]ψ)

Proof of Theorem bisb

Step	Hyp	Ref	Expression
1		bisb.1	. . . 4 ⊢ (φ ↔ ψ)
2	1	biimp 133	. . 3 ⊢ (φ → ψ)
3	2	sbimi 854	. 2 ⊢ ([y / x]φ → [y / x]ψ)
4	1	biimpr 134	. . 3 ⊢ (ψ → φ)
5	4	sbimi 854	. 2 ⊢ ([y / x]ψ → [y / x]φ)
6	3, 5	impbi 139	1 ⊢ ([y / x]φ ↔ [y / x]ψ)

Syntax hints:   ↔ wb 127  [wsb 852

This theorem is referenced by:  sbn2 881  sbor 887  sban 889  sbbi 890  sbco2d 914  sbco3 915  sb7 991  sbex 998  sbabel 1189  sbralie 1439  exss 1881  tfinds2 2405  inopab 2495

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-gen 677

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853

metamath.org