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

Theorem 19.41v 1914
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 1537 . 2  |-  ( ps 
->  A. x ps )
2119.41h 1696 1  |-  ( E. x ( ph  /\  ps )  <->  ( E. x ph  /\  ps ) )
Colors of variables: wff set class
Syntax hints:    /\ wa 104    <-> wb 105   E.wex 1503
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  19.41vv  1915  19.41vvv  1916  19.41vvvv  1917  exdistrv  1922  eeeanv  1945  gencbvex  2798  euxfrdc  2938  euind  2939  dfdif3  3260  r19.9rmv  3529  opabm  4298  eliunxp  4784  relop  4795  dmuni  4855  dmres  4946  dminss  5061  imainss  5062  ssrnres  5089  cnvresima  5136  resco  5151  rnco  5153  coass  5165  xpcom  5193  f11o  5513  fvelrnb  5583  rnoprab  5978  domen  6776  xpassen  6855  genpassl  7552  genpassu  7553
  Copyright terms: Public domain W3C validator