Theorem bnj593 32016

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 1835	. 2 ⊢ (∃𝑥𝜓 → ∃𝑥𝜒)
4	1, 3	syl 17	1 ⊢ (𝜑 → ∃𝑥𝜒)

Syntax hints:   → wi 4  ∃wex 1780

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

This theorem depends on definitions:  df-bi 209  df-ex 1781

This theorem is referenced by:  bnj1266  32083  bnj1304  32091  bnj1379  32102  bnj594  32184  bnj852  32193  bnj908  32203  bnj996  32228  bnj907  32239  bnj1128  32262  bnj1148  32268  bnj1154  32271  bnj1189  32281  bnj1245  32286  bnj1279  32290  bnj1286  32291  bnj1311  32296  bnj1371  32301  bnj1398  32306  bnj1408  32308  bnj1450  32322  bnj1498  32333  bnj1514  32335  bnj1501  32339