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

Theorem 19.41v 1858
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 1491 . 2  |-  ( ps 
->  A. x ps )
2119.41h 1648 1  |-  ( E. x ( ph  /\  ps )  <->  ( E. x ph  /\  ps ) )
Colors of variables: wff set class
Syntax hints:    /\ wa 103    <-> wb 104   E.wex 1453
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1408  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-4 1472  ax-17 1491  ax-ial 1499
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  19.41vv  1859  19.41vvv  1860  19.41vvvv  1861  exdistrv  1864  eeeanv  1885  gencbvex  2706  euxfrdc  2843  euind  2844  dfdif3  3156  r19.9rmv  3424  opabm  4172  eliunxp  4648  relop  4659  dmuni  4719  dmres  4810  dminss  4923  imainss  4924  ssrnres  4951  cnvresima  4998  resco  5013  rnco  5015  coass  5027  xpcom  5055  f11o  5368  fvelrnb  5437  rnoprab  5822  domen  6613  xpassen  6692  genpassl  7300  genpassu  7301
  Copyright terms: Public domain W3C validator