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 2171
Description: If a wff is true, it is true for at least one instance. Deduction form of 19.8a 2170. (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 2170 . 2 (𝜓 → ∃𝑥𝜓)
31, 2syl 17 1 (𝜑 → ∃𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1771
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-12 2167
This theorem depends on definitions:  df-bi 208  df-ex 1772
This theorem is referenced by:  2ax6e  2486  dfmoeu  2611  copsexgw  5372  domtriomlem  9852  axrepnd  10004  axunndlem1  10005  axunnd  10006  axpownd  10011  axacndlem1  10017  axacndlem2  10018  axacndlem3  10019  axacndlem4  10020  axacndlem5  10021  axacnd  10022  pwfseqlem4a  10071  pwfseqlem4  10072  bnj1189  32178  isbasisrelowllem1  34518  isbasisrelowllem2  34519  gneispace  40362  cpcolld  40471  ovncvrrp  42723  ichreuopeq  43512
  Copyright terms: Public domain W3C validator