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

Theorem 19.42v 1878
Description: Special case of Theorem 19.42 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
19.42v (∃𝑥(𝜑𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓))
Distinct variable group:   𝜑,𝑥
Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem 19.42v
StepHypRef Expression
1 ax-17 1506 . 2 (𝜑 → ∀𝑥𝜑)
2119.42h 1665 1 (∃𝑥(𝜑𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓))
Colors of variables: wff set class
Syntax hints:  wa 103  wb 104  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:  exdistr  1881  19.42vv  1883  19.42vvv  1884  4exdistr  1888  cbvex2  1894  2sb5  1958  2sb5rf  1964  rexcom4a  2710  ceqsex2  2726  reuind  2889  2rmorex  2890  sbccomlem  2983  bm1.3ii  4049  opm  4156  eqvinop  4165  uniuni  4372  elco  4705  dmopabss  4751  dmopab3  4752  mptpreima  5032  brprcneu  5414  relelfvdm  5453  fndmin  5527  fliftf  5700  dfoprab2  5818  dmoprab  5852  dmoprabss  5853  fnoprabg  5872  opabex3d  6019  opabex3  6020  eroveu  6520  dmaddpq  7194  dmmulpq  7195  prarloc  7318  ltexprlemopl  7416  ltexprlemlol  7417  ltexprlemopu  7418  ltexprlemupu  7419  shftdm  10601  ntreq0  12311  bdbm1.3ii  13119
  Copyright terms: Public domain W3C validator