Theorem bnj593 34409

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  34475  bnj1304  34483  bnj1379  34494  bnj594  34576  bnj852  34585  bnj908  34595  bnj996  34620  bnj907  34631  bnj1128  34654  bnj1148  34660  bnj1154  34663  bnj1189  34673  bnj1245  34678  bnj1279  34682  bnj1286  34683  bnj1311  34688  bnj1371  34693  bnj1398  34698  bnj1408  34700  bnj1450  34714  bnj1498  34725  bnj1514  34727  bnj1501  34731