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

Theorem 19.42v 1834
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 1464 . 2  |-  ( ph  ->  A. x ph )
2119.42h 1622 1  |-  ( E. x ( ph  /\  ps )  <->  ( ph  /\  E. x 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:  exdistr  1835  19.42vv  1836  19.42vvv  1837  4exdistr  1841  cbvex2  1845  2sb5  1907  2sb5rf  1913  rexcom4a  2643  ceqsex2  2659  reuind  2818  2rmorex  2819  sbccomlem  2911  bm1.3ii  3952  opm  4052  eqvinop  4061  uniuni  4264  elco  4590  dmopabss  4636  dmopab3  4637  mptpreima  4911  brprcneu  5282  relelfvdm  5320  fndmin  5390  fliftf  5560  dfoprab2  5678  dmoprab  5711  dmoprabss  5712  fnoprabg  5728  opabex3d  5874  opabex3  5875  eroveu  6363  dmaddpq  6917  dmmulpq  6918  prarloc  7041  ltexprlemopl  7139  ltexprlemlol  7140  ltexprlemopu  7141  ltexprlemupu  7142  shftdm  10221  bdbm1.3ii  11439
  Copyright terms: Public domain W3C validator