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

Theorem 19.43 1616
 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 361 . . . 4
21exbii 1593 . . 3
3 19.35 1611 . . 3
4 alnex 1553 . . . 4
54imbi1i 317 . . 3
62, 3, 53bitri 264 . 2
7 df-or 361 . 2
86, 7bitr4i 245 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 178   wo 359  wal 1550  wex 1551 This theorem is referenced by:  19.34  1676  19.44  1899  19.45  1900  rexun  3529  unipr  4031  uniun  4036  unopab  4287  zfpair  4404  dmun  5079  coundi  5374  coundir  5375  kmlem16  8050  vdwapun  13347  usgraedg4  21411  pm10.42  27550 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-ex 1552
 Copyright terms: Public domain W3C validator