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

Theorem 19.42vv 1930
 Description: Theorem 19.42 of [Margaris] p. 90 with 2 quantifiers. (Contributed by NM, 16-Mar-1995.)
Assertion
Ref Expression
19.42vv
Distinct variable groups:   ,   ,
Allowed substitution hints:   (,)

Proof of Theorem 19.42vv
StepHypRef Expression
1 exdistr 1929 . 2
2 19.42v 1928 . 2
31, 2bitri 241 1
 Colors of variables: wff set class Syntax hints:   wb 177   wa 359  wex 1550 This theorem is referenced by:  19.42vvv  1931  exdistr2  1932  3exdistr  1933  ceqsex3v  2994  ceqsex4v  2995  ceqsex8v  2997  elvvv  4937  dfoprab2  6121  resoprab  6166  oprabex3  6188  ov3  6210  ov6g  6211  xpassen  7202  axaddf  9020  axmulf  9021  usgraedg4  21406  qqhval2  24366  el2wlkonot  28336  el2spthonot  28337  el2wlkonotot0  28339  bnj996  29326  dvhopellsm  31915 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-11 1761 This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-nf 1554
 Copyright terms: Public domain W3C validator