Theorem 19.8a 1376

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 1319	. . 3 |- (A.x -. ph -> -. ph)
2	1	con2i 113	. 2 |- (ph -> -. A.x -. ph)
3		df-ex 1327	. 2 |- (E.xph <-> -. A.x -. ph)
4	2, 3	sylibr 217	1 |- (ph -> E.xph)

Syntax hints:  -. wn 2   -> wi 3  A.wal 1296  E.wex 1326

This theorem is referenced by:  19.2 1377  19.9 1383  excomim 1392  19.23 1411  19.23bi 1414  19.38 1432  nexr 1455  qexmid 1479  sbequ1 1542  ax11indn 1757  mo 1787  mo2 1795  euor2 1839  euor2OLD 1840  2moex 1843  2euex 1844  2moswap 1848  2exeu 1850  2mo 1851  ra4e 2156  ceqex 2391  mo2icl 2434  elrabsf 2486  ssuni 3201  ssuniOLD 3202  intab 3247  axnulALT 3443  copsexg 3537  dmcosseq 4214  dmcosseqOLD 4215  dminss 4330  imainss 4331  relssdmrn 4416  funeu 4444  funeuOLD 4445  tz6.12-1 4693  tz9.12lem1 5770  hta 5858  aceq3lem 5894  ac6lem 5916  axextnd 6095  axrepnd 6098  axunndlem1 6099  axunnd 6100  axpowndlem2 6102  axpownd 6105  axregndlem1 6106  axregnd 6108  axacndlem1 6111  axacndlem2 6112  axacndlem3 6113  axacndlem4 6114  axacndlem5 6115  axacnd 6116  cmsss 9275  chcmhi 10746  xfree 12016  bnj1193 12970  bnj1121 13421  amosym1 14250  finminlem 15367  inficlALT 15372  neibastop2lem3 15521  filnetlem5 15644  pm11.58 16347  ax10ext 16364  iotavalsb 16398

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

This theorem depends on definitions:  df-bi 164  df-ex 1327

Copyright terms: Public domain