Theorem 19.8a 1070

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 1014	. . 3 |- (A.x -. ph -> -. ph)
2	1	con2i 102	. 2 |- (ph -> -. A.x -. ph)
3		df-ex 1022	. 2 |- (E.xph <-> -. A.x -. ph)
4	2, 3	sylibr 207	1 |- (ph -> E.xph)

Syntax hints:  -. wn 2   -> wi 3  A.wal 995  E.wex 1021

This theorem is referenced by:  19.2 1071  19.9 1077  excomim 1086  19.23 1104  19.23bi 1106  19.38 1122  qexmid 1162  sbequ1 1220  ax11indn 1408  mo 1435  mo2 1442  euor2 1480  2moex 1483  2moswap 1487  2exeu 1489  2mo 1490  ra4e 1742  ceqex 1933  mo2icl 1970  elrabsf 2013  ssuni 2576  intab 2614  axnul2 2763  dmcosseq 3422  dminss 3519  imainss 3520  relssdr 3570  funeu 3594  tz6.12-1 3793  tz9.12lem1 4721  hta 4790  aceq3lem 4794  ac6lem 4816  axextnd 5008  axrepnd 5011  axunndlem1 5012  axunnd 5013  axpowndlem2 5015  axpownd 5018  axregndlem1 5019  axregnd 5021  axacndlem1 5024  axacndlem2 5025  axacndlem3 5026  axacndlem4 5027  axacndlem5 5028  axacnd 5029  cmsss 8082  chcmhi 9196

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

This theorem depends on definitions:  df-bi 154  df-ex 1022

Copyright terms: Public domain