Theorem bnj593 34880

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

Syntax hints:   → wi 4  ∃wex 1781

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

This theorem depends on definitions:  df-bi 207  df-ex 1782

This theorem is referenced by:  bnj1266  34946  bnj1304  34954  bnj1379  34965  bnj594  35047  bnj852  35056  bnj908  35066  bnj996  35091  bnj907  35102  bnj1128  35125  bnj1148  35131  bnj1154  35134  bnj1189  35144  bnj1245  35149  bnj1279  35153  bnj1286  35154  bnj1311  35159  bnj1371  35164  bnj1398  35169  bnj1408  35171  bnj1450  35185  bnj1498  35196  bnj1514  35198  bnj1501  35202