MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sbimi Unicode version

Theorem sbimi 1633
Description: Infer substitution into antecedent and consequent of an implication. (Contributed by NM, 25-Jun-1998.)
Hypothesis
Ref Expression
sbimi.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
sbimi  |-  ( [ y  /  x ] ph  ->  [ y  /  x ] ps )

Proof of Theorem sbimi
StepHypRef Expression
1 sbimi.1 . . . 4  |-  ( ph  ->  ps )
21imim2i 13 . . 3  |-  ( ( x  =  y  ->  ph )  ->  ( x  =  y  ->  ps ) )
31anim2i 552 . . . 4  |-  ( ( x  =  y  /\  ph )  ->  ( x  =  y  /\  ps )
)
43eximi 1563 . . 3  |-  ( E. x ( x  =  y  /\  ph )  ->  E. x ( x  =  y  /\  ps ) )
52, 4anim12i 549 . 2  |-  ( ( ( x  =  y  ->  ph )  /\  E. x ( x  =  y  /\  ph )
)  ->  ( (
x  =  y  ->  ps )  /\  E. x
( x  =  y  /\  ps ) ) )
6 df-sb 1630 . 2  |-  ( [ y  /  x ] ph 
<->  ( ( x  =  y  ->  ph )  /\  E. x ( x  =  y  /\  ph )
) )
7 df-sb 1630 . 2  |-  ( [ y  /  x ] ps 
<->  ( ( x  =  y  ->  ps )  /\  E. x ( x  =  y  /\  ps ) ) )
85, 6, 73imtr4i 257 1  |-  ( [ y  /  x ] ph  ->  [ y  /  x ] ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358   E.wex 1528   [wsb 1629
This theorem is referenced by:  sbbii  1634  sb6f  1979  hbsb3  1983  sbi2  2004  sbco  2023  sbidm  2025  sbal1  2065  sbal  2066  ballotlemodife  23056  fmptdF  23221  funcnv4mpt  23237  disjdsct  23369  measiuns  23544
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-sb 1630
  Copyright terms: Public domain W3C validator