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

Theorem 19.41v 1874
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 1506 . 2  |-  ( ps 
->  A. x ps )
2119.41h 1663 1  |-  ( E. x ( ph  /\  ps )  <->  ( E. x ph  /\  ps ) )
Colors of variables: wff set class
Syntax hints:    /\ wa 103    <-> wb 104   E.wex 1468
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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  19.41vv  1875  19.41vvv  1876  19.41vvvv  1877  exdistrv  1882  eeeanv  1903  gencbvex  2727  euxfrdc  2865  euind  2866  dfdif3  3181  r19.9rmv  3449  opabm  4197  eliunxp  4673  relop  4684  dmuni  4744  dmres  4835  dminss  4948  imainss  4949  ssrnres  4976  cnvresima  5023  resco  5038  rnco  5040  coass  5052  xpcom  5080  f11o  5393  fvelrnb  5462  rnoprab  5847  domen  6638  xpassen  6717  genpassl  7325  genpassu  7326
  Copyright terms: Public domain W3C validator