Theorem 19.8a 1029

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 973	. . 3 |- (A.x -. ph -> -. ph)
2	1	con2i 97	. 2 |- (ph -> -. A.x -. ph)
3		df-ex 981	. 2 |- (E.xph <-> -. A.x -. ph)
4	2, 3	sylibr 200	1 |- (ph -> E.xph)

Syntax hints:  -. wn 2   -> wi 3  A.wal 954  E.wex 980

This theorem is referenced by:  19.2 1030  19.9 1036  excomim 1045  19.23 1063  19.23bi 1065  19.38 1081  qexmid 1121  sbequ1 1178  ax11indn 1366  mo 1393  mo2 1400  euor2 1437  2moex 1440  2moswap 1444  2exeu 1446  2mo 1447  ra4e 1695  ceqex 1886  mo2icl 1923  elrabsf 1963  ssuni 2522  intab 2560  axnul2 2708  dmcosseq 3365  dminss 3462  imainss 3463  relssdr 3513  funeu 3537  tz6.12-1 3736  tz9.12lem1 4659  hta 4728  aceq3lem 4732  ac6lem 4754  axextnd 4943  axrepnd 4946  axunndlem1 4947  axunnd 4948  axpowndlem2 4950  axpownd 4953  axregndlem1 4954  axregnd 4956  axacndlem1 4959  axacndlem2 4960  axacndlem3 4961  axacndlem4 4962  axacndlem5 4963  axacnd 4964  cmsss 7997  chcmh 9113

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

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

Copyright terms: Public domain