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

Theorem sbimi 1659
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 14 . . 3  |-  ( ( x  =  y  ->  ph )  ->  ( x  =  y  ->  ps ) )
31anim2i 553 . . . 4  |-  ( ( x  =  y  /\  ph )  ->  ( x  =  y  /\  ps )
)
43eximi 1582 . . 3  |-  ( E. x ( x  =  y  /\  ph )  ->  E. x ( x  =  y  /\  ps ) )
52, 4anim12i 550 . 2  |-  ( ( ( x  =  y  ->  ph )  /\  E. x ( x  =  y  /\  ph )
)  ->  ( (
x  =  y  ->  ps )  /\  E. x
( x  =  y  /\  ps ) ) )
6 df-sb 1656 . 2  |-  ( [ y  /  x ] ph 
<->  ( ( x  =  y  ->  ph )  /\  E. x ( x  =  y  /\  ph )
) )
7 df-sb 1656 . 2  |-  ( [ y  /  x ] ps 
<->  ( ( x  =  y  ->  ps )  /\  E. x ( x  =  y  /\  ps ) ) )
85, 6, 73imtr4i 258 1  |-  ( [ y  /  x ] ph  ->  [ y  /  x ] ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359   E.wex 1547   [wsb 1655
This theorem is referenced by:  sbbii  1660  sb6f  2072  hbsb3  2076  sbi2  2097  sbco  2116  sbidm  2118  sbal1  2160  sbal  2161  fmptdF  23911  funcnv4mpt  23926  disjdsct  23931  measiuns  24365  ballotlemodife  24534  hbsb3NEW7  28880  sbi2NEW7  28900  sbcoNEW7  28917  sbidmNEW7  28919  sbal1NEW7  28948  sbalNEW7  28949  sb6fNEW7  28966
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-sb 1656
  Copyright terms: Public domain W3C validator