New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  sbbii GIF version

Theorem sbbii 1653
 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 ([y / x]φ ↔ [y / x]ψ)

Proof of Theorem sbbii
StepHypRef Expression
1 sbbii.1 . . . 4 (φψ)
21biimpi 186 . . 3 (φψ)
32sbimi 1652 . 2 ([y / x]φ → [y / x]ψ)
41biimpri 197 . . 3 (ψφ)
54sbimi 1652 . 2 ([y / x]ψ → [y / x]φ)
63, 5impbii 180 1 ([y / x]φ ↔ [y / x]ψ)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 176  [wsb 1648 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557 This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-sb 1649 This theorem is referenced by:  sbn  2062  sbor  2066  sban  2069  sb3an  2070  sbbi  2071  sbco2d  2087  sbco3  2088  equsb3  2102  elsb3  2103  elsb4  2104  dfsb7  2119  sb7f  2120  sbex  2128  sbmo  2234  2eu6  2289  eqsb3  2454  clelsb3  2455  sbabel  2515  sbralie  2848  sbcco  3068
 Copyright terms: Public domain W3C validator