MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sbi1 Structured version   Visualization version   Unicode version
Theorem sbi1 2392
Description: Removal of implication from substitution. (Contributed by NM, 14-May-1993.)
Assertion
Ref Expression
sbi1 |- ( [ y / x ] ( ph -> ps ) -> ( [ y / x ] ph -> [ y / x ] ps ) )
Proof of Theorem sbi1
StepHypRef Expression
1 sbequ2 1882 . . . . 5 |- ( x = y -> ( [ y / x ] ph -> ph ) )
2 sbequ2 1882 . . . . 5 |- ( x = y -> ( [ y / x ] ( ph -> ps ) -> ( ph -> ps ) ) )
31, 2syl5d 73 . . . 4 |- ( x = y -> ( [ y / x ] ( ph -> ps ) -> ( [ y / x ] ph -> ps ) ) )
4 sbequ1 2110 . . . 4 |- ( x = y -> ( ps -> [ y / x ] ps ) )
53, 4syl6d 75 . . 3 |- ( x = y -> ( [ y / x ] ( ph -> ps ) -> ( [ y / x ] ph -> [ y / x ] ps ) ) )
65sps 2055 . 2 |- ( A. x x = y -> ( [ y / x ] ( ph -> ps ) -> ( [ y / x ] ph -> [ y / x ] ps ) ) )
7 sb4 2356 . . 3 |- ( -. A. x x = y -> ( [ y / x ] ph -> A. x ( x = y -> ph ) ) )
8 sb4 2356 . . . 4 |- ( -. A. x x = y -> ( [ y / x ] ( ph -> ps ) -> A. x ( x = y -> ( ph -> ps ) ) ) )
9 ax-2 7 . . . . . 6 |- ( ( x = y -> ( ph -> ps ) ) -> ( ( x = y -> ph ) -> ( x = y -> ps ) ) )
109al2imi 1743 . . . . 5 |- ( A. x ( x = y -> ( ph -> ps ) ) -> ( A. x ( x = y -> ph ) -> A. x ( x = y -> ps ) ) )
11 sb2 2352 . . . . 5 |- ( A. x ( x = y -> ps ) -> [ y / x ] ps )
1210, 11syl6 35 . . . 4 |- ( A. x ( x = y -> ( ph -> ps ) ) -> ( A. x ( x = y -> ph ) -> [ y / x ] ps ) )
138, 12syl6 35 . . 3 |- ( -. A. x x = y -> ( [ y / x ] ( ph -> ps ) -> ( A. x ( x = y -> ph ) -> [ y / x ] ps ) ) )
147, 13syl5d 73 . 2 |- ( -. A. x x = y -> ( [ y / x ] ( ph -> ps ) -> ( [ y / x ] ph -> [ y / x ] ps ) ) )
156, 14pm2.61i 176 1 |- ( [ y / x ] ( ph -> ps ) -> ( [ y / x ] ph -> [ y / x ] ps ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3   -> wi 4   A.wal 1481   [wsb 1880
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-10 2019  ax-12 2047  ax-13 2246
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ex 1705  df-nf 1710  df-sb 1881
This theorem is referenced by:  spsbim  2394  sbim  2395  2sb5ndVD  39146  2sb5ndALT  39168
  Copyright terms: Public domain W3C validator