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

Theorem sbimi 1642
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 1566 . . 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 1639 . 2  |-  ( [ y  /  x ] ph 
<->  ( ( x  =  y  ->  ph )  /\  E. x ( x  =  y  /\  ph )
) )
7 df-sb 1639 . 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 1531   [wsb 1638
This theorem is referenced by:  sbbii  1643  sb6f  1992  hbsb3  1996  sbi2  2017  sbco  2036  sbidm  2038  sbal1  2078  sbal  2079  ballotlemodife  23072  fmptdF  23236  funcnv4mpt  23252  disjdsct  23384  measiuns  23559  hbsb3NEW7  29519  sbi2NEW7  29539  sbcoNEW7  29556  sbidmNEW7  29558  sbal1NEW7  29587  sbalNEW7  29588  sb6fNEW7  29605
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-sb 1639
  Copyright terms: Public domain W3C validator