Theorem 19.8a 1025

Description: If a wff is true, it is true for at least one instance. Special case of Theorem 19.8 of [Margaris] p. 89.

Assertion

Ref	Expression
19.8a	|- (ph -> E.xph)

Proof of Theorem 19.8a

Step	Hyp	Ref	Expression
1		ax-4 970	. . 3 |- (A.x -. ph -> -. ph)
2	1	con2i 97	. 2 |- (ph -> -. A.x -. ph)
3		df-ex 978	. 2 |- (E.xph <-> -. A.x -. ph)
4	2, 3	sylibr 200	1 |- (ph -> E.xph)

Syntax hints:  -. wn 2   -> wi 3  A.wal 951  E.wex 977

This theorem is referenced by:  19.2 1026  19.9 1032  excomim 1041  19.23 1059  19.23bi 1061  19.38 1077  qexmid 1117  sbequ1 1174  ax11indn 1359  mo 1386  mo2 1393  euor2 1430  2moex 1433  2moswap 1437  2exeu 1439  2mo 1440  ra4e 1687  ceqex 1877  mo2icl 1914  elrabsf 1953  ssuni 2512  intab 2550  axnul2 2698  dmcosseq 3349  dminss 3448  imainss 3449  relssdr 3499  funeu 3523  tz6.12-1 3721  tz9.12lem1 4631  hta 4700  aceq3lem 4704  ac6lem 4726  axextnd 4915  axrepnd 4918  axunndlem1 4919  axunnd 4920  axpowndlem2 4922  axpownd 4925  axregndlem1 4926  axregnd 4928  axacndlem1 4931  axacndlem2 4932  axacndlem3 4933  axacndlem4 4934  axacndlem5 4935  axacnd 4936  cmsss 7931  chcmh 9034

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 970

This theorem depends on definitions:  df-bi 147  df-ex 978

Copyright terms: Public domain