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

Theorem 19.41v 1824
Description: Special case of Theorem 19.41 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
19.41v  |-  ( E. x ( ph  /\  ps )  <->  ( E. x ph  /\  ps ) )
Distinct variable group:    ps, x
Allowed substitution hint:    ph( x)

Proof of Theorem 19.41v
StepHypRef Expression
1 ax-17 1460 . 2  |-  ( ps 
->  A. x ps )
2119.41h 1616 1  |-  ( E. x ( ph  /\  ps )  <->  ( E. x ph  /\  ps ) )
Colors of variables: wff set class
Syntax hints:    /\ wa 102    <-> wb 103   E.wex 1422
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441  ax-17 1460  ax-ial 1468
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  19.41vv  1825  19.41vvv  1826  19.41vvvv  1827  eeeanv  1850  gencbvex  2646  euxfrdc  2779  euind  2780  r19.9rmv  3340  opabm  4043  eliunxp  4503  relop  4514  dmuni  4573  dmres  4660  dminss  4768  imainss  4769  ssrnres  4793  cnvresima  4840  resco  4855  rnco  4857  coass  4869  xpcom  4894  f11o  5190  fvelrnb  5253  rnoprab  5618  domen  6298  xpassen  6374  genpassl  6776  genpassu  6777
  Copyright terms: Public domain W3C validator