Theorem bnj593 34432

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)

Hypotheses

Ref	Expression
bnj593.1	⊢ (𝜑 → ∃𝑥𝜓)
bnj593.2	⊢ (𝜓 → 𝜒)

Assertion

Ref	Expression
bnj593	⊢ (𝜑 → ∃𝑥𝜒)

Proof of Theorem bnj593

Step	Hyp	Ref	Expression
1		bnj593.1	. 2 ⊢ (𝜑 → ∃𝑥𝜓)
2		bnj593.2	. . 3 ⊢ (𝜓 → 𝜒)
3	2	eximi 1829	. 2 ⊢ (∃𝑥𝜓 → ∃𝑥𝜒)
4	1, 3	syl 17	1 ⊢ (𝜑 → ∃𝑥𝜒)

Syntax hints:   → wi 4  ∃wex 1773

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803

This theorem depends on definitions:  df-bi 206  df-ex 1774

This theorem is referenced by:  bnj1266  34498  bnj1304  34506  bnj1379  34517  bnj594  34599  bnj852  34608  bnj908  34618  bnj996  34643  bnj907  34654  bnj1128  34677  bnj1148  34683  bnj1154  34686  bnj1189  34696  bnj1245  34701  bnj1279  34705  bnj1286  34706  bnj1311  34711  bnj1371  34716  bnj1398  34721  bnj1408  34723  bnj1450  34737  bnj1498  34748  bnj1514  34750  bnj1501  34754

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »