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

Theorem 19.41v 1830
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 1464 . 2  |-  ( ps 
->  A. x ps )
2119.41h 1620 1  |-  ( E. x ( ph  /\  ps )  <->  ( E. x ph  /\  ps ) )
Colors of variables: wff set class
Syntax hints:    /\ wa 102    <-> wb 103   E.wex 1426
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 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445  ax-17 1464  ax-ial 1472
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  19.41vv  1831  19.41vvv  1832  19.41vvvv  1833  eeeanv  1856  gencbvex  2665  euxfrdc  2801  euind  2802  dfdif3  3110  r19.9rmv  3373  opabm  4107  eliunxp  4575  relop  4586  dmuni  4646  dmres  4734  dminss  4846  imainss  4847  ssrnres  4873  cnvresima  4920  resco  4935  rnco  4937  coass  4949  xpcom  4977  f11o  5286  fvelrnb  5352  rnoprab  5731  domen  6466  xpassen  6544  genpassl  7081  genpassu  7082
  Copyright terms: Public domain W3C validator