MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  19.8ad Structured version   Visualization version   GIF version

Theorem 19.8ad 2170
Description: If a wff is true, it is true for at least one instance. Deduction form of 19.8a 2169. (Contributed by DAW, 13-Feb-2017.)
Hypothesis
Ref Expression
19.8ad.1 (𝜑𝜓)
Assertion
Ref Expression
19.8ad (𝜑 → ∃𝑥𝜓)

Proof of Theorem 19.8ad
StepHypRef Expression
1 19.8ad.1 . 2 (𝜑𝜓)
2 19.8a 2169 . 2 (𝜓 → ∃𝑥𝜓)
31, 2syl 17 1 (𝜑 → ∃𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1773
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-12 2166
This theorem depends on definitions:  df-bi 206  df-ex 1774
This theorem is referenced by:  2ax6e  2464  dfmoeu  2524  copsexgw  5492  domtriomlem  10467  axrepnd  10619  axunndlem1  10620  axunnd  10621  axpownd  10626  axacndlem1  10632  axacndlem2  10633  axacndlem3  10634  axacndlem4  10635  axacndlem5  10636  axacnd  10637  pwfseqlem4a  10686  pwfseqlem4  10687  bnj1189  34768  isbasisrelowllem1  36962  isbasisrelowllem2  36963  gneispace  43703  cpcolld  43834  ovncvrrp  46087  ichreuopeq  46947
  Copyright terms: Public domain W3C validator