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

Theorem 19.43 1612
 Description: Theorem 19.43 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 27-Jun-2014.)
Assertion
Ref Expression
19.43

Proof of Theorem 19.43
StepHypRef Expression
1 df-or 360 . . . 4
21exbii 1589 . . 3
3 19.35 1607 . . 3
4 alnex 1549 . . . 4
54imbi1i 316 . . 3
62, 3, 53bitri 263 . 2
7 df-or 360 . 2
86, 7bitr4i 244 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 177   wo 358  wal 1546  wex 1547 This theorem is referenced by:  19.34  1671  19.44  1894  19.45  1895  rexun  3487  unipr  3989  uniun  3994  unopab  4244  zfpair  4361  dmun  5035  coundi  5330  coundir  5331  kmlem16  8001  vdwapun  13297  usgraedg4  21359  pm10.42  27427 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-or 360  df-an 361  df-ex 1548
 Copyright terms: Public domain W3C validator