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

Theorem sban 2140
Description: Conjunction inside and outside of a substitution are equivalent. (Contributed by NM, 14-May-1993.)
Assertion
Ref Expression
sban

Proof of Theorem sban
StepHypRef Expression
1 sbn 2132 . . 3
2 sbim 2136 . . . 4
3 sbn 2132 . . . . 5
43imbi2i 312 . . . 4
52, 4bitri 249 . . 3
61, 5xchbinx 310 . 2
7 df-an 371 . . 3
87sbbii 1746 . 2
9 df-an 371 . 2
106, 8, 93bitr4i 277 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  <->wb 184  /\wa 369  [wsb 1739
This theorem is referenced by:  sb3an  2141  sbbi  2142  mopickOLD  2357  sbabel  2650  sbabelOLD  2651  cbvreu  3082  sbcan  3370  sbcangOLD  3371  rmo3  3429  inab  3765  difab  3766  exss  4715  inopab  5138  mo5f  27383  rmo3f  27394  iuninc  27428  suppss2f  27477  fmptdF  27495  disjdsct  27521  esumpfinvalf  28082  measiuns  28188  ballotlemodife  28436  ellimcabssub0  31623  sb5ALT  33295  2uasbanh  33334  2uasbanhVD  33711  sb5ALTVD  33713
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