Theorem 19.8a 712

Description: If a wff is true, it is true for at least one instance.

Assertion

Ref	Expression
19.8a	⊢ (φ → ∃xφ)

Proof of Theorem 19.8a

Step	Hyp	Ref	Expression
1		ax-4 673	. . 3 ⊢ (∀x ¬ φ → ¬ φ)
2	1	con2i 89	. 2 ⊢ (φ → ¬ ∀x ¬ φ)
3		df-ex 679	. 2 ⊢ (∃xφ ↔ ¬ ∀x ¬ φ)
4	2, 3	sylibr 175	1 ⊢ (φ → ∃xφ)

Syntax hints:  ¬ wn 1   → wi 2  ∀wal 672  ∃wex 678

This theorem is referenced by:  19.2 713  19.9r 718  excomim 727  19.23 745  19.23bi 747  19.38 760  qexmid 796  sbequ1 863  mo 1020  mo2 1026  2moex 1060  2moswap 1064  2exeu 1066  ra4e 1244  ceqex 1410  mo2icl 1434  elrabsf 1456  ssuni 1937  dmcosseq 2572  dminss 2648  imainss 2649  relssdr 2668  funeu 2685  tz6.12-1 2842  tz9.12lem1 3503  aceq3lem 3555  ac6lem 3575  hta 3619  axextnd 3737  axrepnd 3740  axunndlem1 3741  axunnd 3742  axpowndlem2 3744  axpownd 3747  axregndlem1 3748  axregnd 3750  axacndlem1 3753  axacndlem2 3754  axacndlem3 3755  axacndlem4 3756  axacndlem5 3757  axacnd 3758  chcmh 5148

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

This theorem depends on definitions:  df-bi 128  df-ex 679

metamath.org