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

Theorem sbim 2136
Description: Implication inside and outside of substitution are equivalent. (Contributed by NM, 14-May-1993.)
Assertion
Ref Expression
sbim

Proof of Theorem sbim
StepHypRef Expression
1 sbi1 2133 . 2
2 sbi2 2134 . 2
31, 2impbii 188 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  [wsb 1739
This theorem is referenced by:  sbrim  2137  sblim  2138  sbor  2139  sban  2140  sbbi  2142  sbequ8ALT  2148  sbcimg  3369  mo5f  27383  iuninc  27428  suppss2f  27477  esumpfinvalf  28082  wl-sbrimt  29998  wl-sblimt  29999  ellimcabssub0  31623  bj-sbnf  34412  frege58bcor  37930  frege60b  37932  frege65b  37937  frege70  37961
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-12 1854  ax-13 1999
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1613  df-nf 1617  df-sb 1740
  Copyright terms: Public domain W3C validator