Theorem sbbii 1814

Description: Infer substitution into both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
sbbii.1	|- ( ph <-> ps )

Assertion

Ref	Expression
sbbii	|- ( [ y / x ] ph <-> [ y / x ] ps )

Proof of Theorem sbbii

Step	Hyp	Ref	Expression
1		sbbii.1	. . . 4 |- ( ph <-> ps )
2	1	biimpi 120	. . 3 |- ( ph -> ps )
3	2	sbimi 1813	. 2 |- ( [ y / x ] ph -> [ y / x ] ps )
4	1	biimpri 133	. . 3 |- ( ps -> ph )
5	4	sbimi 1813	. 2 |- ( [ y / x ] ps -> [ y / x ] ph )
6	3, 5	impbii 126	1 |- ( [ y / x ] ph <-> [ y / x ] ps )

Syntax hints:   <-> wb 105   [wsb 1811

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-ial 1583

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

This theorem is referenced by:  sbco2vh  1999  equsb3  2005  sbn  2006  sbim  2007  sbor  2008  sban  2009  sb3an  2012  sbbi  2013  sbco2h  2018  sbco2d  2020  sbco2vd  2021  sbco3v  2023  sbco3  2028  sbcom2v2  2040  sbcom2  2041  dfsb7  2045  sb7f  2046  sb7af  2047  sbal  2054  sbal1  2056  sbex  2058  sbco4lem  2060  sbco4  2061  sbmo  2140  elsb1  2210  elsb2  2211  eqsb1  2336  clelsb1  2337  clelsb2  2338  cbvabw  2357  clelsb1f  2388  sbabel  2411  sbralie  2796  sbcco  3064  exss  4343  inopab  4887  isarep1  5442  bezoutlemnewy  12692