Theorem bnj593 34742

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 1779

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

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

This theorem is referenced by:  bnj1266  34808  bnj1304  34816  bnj1379  34827  bnj594  34909  bnj852  34918  bnj908  34928  bnj996  34953  bnj907  34964  bnj1128  34987  bnj1148  34993  bnj1154  34996  bnj1189  35006  bnj1245  35011  bnj1279  35015  bnj1286  35016  bnj1311  35021  bnj1371  35026  bnj1398  35031  bnj1408  35033  bnj1450  35047  bnj1498  35058  bnj1514  35060  bnj1501  35064