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 2173
Description: If a wff is true, it is true for at least one instance. Deduction form of 19.8a 2172. (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 2172 . 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 1904  ax-6 1963  ax-7 2008  ax-12 2169
This theorem depends on definitions:  df-bi 209  df-ex 1774
This theorem is referenced by:  2ax6e  2487  dfmoeu  2612  copsexgw  5372  domtriomlem  9856  axrepnd  10008  axunndlem1  10009  axunnd  10010  axpownd  10015  axacndlem1  10021  axacndlem2  10022  axacndlem3  10023  axacndlem4  10024  axacndlem5  10025  axacnd  10026  pwfseqlem4a  10075  pwfseqlem4  10076  bnj1189  32269  isbasisrelowllem1  34623  isbasisrelowllem2  34624  gneispace  40469  cpcolld  40579  ovncvrrp  42831  ichreuopeq  43620
  Copyright terms: Public domain W3C validator