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

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

Proof of Theorem 19.42v
StepHypRef Expression
1 ax-17 1489 . 2  |-  ( ph  ->  A. x ph )
2119.42h 1648 1  |-  ( E. x ( ph  /\  ps )  <->  ( ph  /\  E. x ps ) )
Colors of variables: wff set class
Syntax hints:    /\ wa 103    <-> wb 104   E.wex 1451
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 1406  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-4 1470  ax-17 1489  ax-ial 1497
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  exdistr  1861  19.42vv  1863  19.42vvv  1864  4exdistr  1868  cbvex2  1872  2sb5  1934  2sb5rf  1940  rexcom4a  2682  ceqsex2  2698  reuind  2860  2rmorex  2861  sbccomlem  2953  bm1.3ii  4017  opm  4124  eqvinop  4133  uniuni  4340  elco  4673  dmopabss  4719  dmopab3  4720  mptpreima  5000  brprcneu  5380  relelfvdm  5419  fndmin  5493  fliftf  5666  dfoprab2  5784  dmoprab  5818  dmoprabss  5819  fnoprabg  5838  opabex3d  5985  opabex3  5986  eroveu  6486  dmaddpq  7151  dmmulpq  7152  prarloc  7275  ltexprlemopl  7373  ltexprlemlol  7374  ltexprlemopu  7375  ltexprlemupu  7376  shftdm  10545  ntreq0  12207  bdbm1.3ii  12923
  Copyright terms: Public domain W3C validator