ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  19.42vv Unicode version

Theorem 19.42vv 1788
Description: Theorem 19.42 of [Margaris] p. 90 with 2 quantifiers. (Contributed by NM, 16-Mar-1995.)
Assertion
Ref Expression
19.42vv  |-  ( E. x E. y (
ph  /\  ps )  <->  (
ph  /\  E. x E. y ps ) )
Distinct variable groups:    ph, x    ph, y
Allowed substitution hints:    ps( x, y)

Proof of Theorem 19.42vv
StepHypRef Expression
1 exdistr 1787 . 2  |-  ( E. x E. y (
ph  /\  ps )  <->  E. x ( ph  /\  E. y ps ) )
2 19.42v 1786 . 2  |-  ( E. x ( ph  /\  E. y ps )  <->  ( ph  /\ 
E. x E. y ps ) )
31, 2bitri 173 1  |-  ( E. x E. y (
ph  /\  ps )  <->  (
ph  /\  E. x E. y ps ) )
Colors of variables: wff set class
Syntax hints:    /\ wa 97    <-> wb 98   E.wex 1381
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  19.42vvv  1789  19.42vvvv  1790  exdistr2  1791  3exdistr  1792  ceqsex3v  2596  ceqsex4v  2597  elvvv  4403  dfoprab2  5552  resoprab  5597  ovi3  5637  ov6g  5638  oprabex3  5756  xpassen  6304  enq0enq  6529  enq0sym  6530  nqnq0pi  6536
  Copyright terms: Public domain W3C validator