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

Theorem 19.8a 1482
Description: If a wff is true, it is true for at least one instance. Special case of Theorem 19.8 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
19.8a (𝜑 → ∃𝑥𝜑)

Proof of Theorem 19.8a
StepHypRef Expression
1 id 19 . . 3 (∃𝑥𝜑 → ∃𝑥𝜑)
2 hbe1 1384 . . . 4 (∃𝑥𝜑 → ∀𝑥𝑥𝜑)
3219.23h 1387 . . 3 (∀𝑥(𝜑 → ∃𝑥𝜑) ↔ (∃𝑥𝜑 → ∃𝑥𝜑))
41, 3mpbir 134 . 2 𝑥(𝜑 → ∃𝑥𝜑)
54spi 1429 1 (𝜑 → ∃𝑥𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1241  wex 1381
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  19.23bi  1483  exim  1490  19.43  1519  hbex  1527  19.2  1529  19.9t  1533  19.9h  1534  excomim  1553  19.38  1566  nexr  1582  sbequ1  1651  equs5e  1676  exdistrfor  1681  sbcof2  1691  mo2n  1928  euor2  1958  2moex  1986  2euex  1987  2moswapdc  1990  2exeu  1992  rspe  2370  rsp2e  2372  ceqex  2671  vn0m  3232  intab  3644  copsexg  3981  eusv2nf  4188  dmcosseq  4603  dminss  4738  imainss  4739  relssdmrn  4841  oprabid  5537  tfrlemibxssdm  5941  nqprl  6647  nqpru  6648  ltsopr  6692  ltexprlemm  6696  recexprlemopl  6721  recexprlemopu  6723
  Copyright terms: Public domain W3C validator