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

Theorem 19.42v 1802
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 1435 . 2 (𝜑 → ∀𝑥𝜑)
2119.42h 1593 1 (∃𝑥(𝜑𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓))
Colors of variables: wff set class
Syntax hints:  wa 101  wb 102  wex 1397
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-4 1416  ax-17 1435  ax-ial 1443
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  exdistr  1803  19.42vv  1804  19.42vvv  1805  4exdistr  1809  cbvex2  1813  2sb5  1875  2sb5rf  1881  rexcom4a  2595  ceqsex2  2611  reuind  2767  2rmorex  2768  sbccomlem  2860  bm1.3ii  3906  opm  3999  eqvinop  4008  uniuni  4211  dmopabss  4575  dmopab3  4576  mptpreima  4842  brprcneu  5199  relelfvdm  5233  fndmin  5302  fliftf  5467  dfoprab2  5580  dmoprab  5613  dmoprabss  5614  fnoprabg  5630  opabex3d  5776  opabex3  5777  eroveu  6228  dmaddpq  6535  dmmulpq  6536  prarloc  6659  ltexprlemopl  6757  ltexprlemlol  6758  ltexprlemopu  6759  ltexprlemupu  6760  shftdm  9651  bdbm1.3ii  10398
  Copyright terms: Public domain W3C validator