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

Theorem sbimi 1664
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 1585 . . 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 1659 . 2  |-  ( [ y  /  x ] ph 
<->  ( ( x  =  y  ->  ph )  /\  E. x ( x  =  y  /\  ph )
) )
7 df-sb 1659 . 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 1550   [wsb 1658
This theorem is referenced by:  sbbii  1665  hbsb3  2095  sbi2  2120  sb6f  2127  sbco  2158  sbidm  2160  sbal1  2202  sbal  2203  fmptdF  24061  funcnv4mpt  24077  disjdsct  24082  measiuns  24563  ballotlemodife  24747  hbsb3NEW7  29481  sbi2NEW7  29501  sbcoNEW7  29519  sbidmNEW7  29521  sbal1NEW7  29552  sbalNEW7  29553  sb6fNEW7  29570
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-sb 1659
  Copyright terms: Public domain W3C validator