Theorem bnj593 33756

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

Syntax hints:   → wi 4  ∃wex 1782

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

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

This theorem is referenced by:  bnj1266  33822  bnj1304  33830  bnj1379  33841  bnj594  33923  bnj852  33932  bnj908  33942  bnj996  33967  bnj907  33978  bnj1128  34001  bnj1148  34007  bnj1154  34010  bnj1189  34020  bnj1245  34025  bnj1279  34029  bnj1286  34030  bnj1311  34035  bnj1371  34040  bnj1398  34045  bnj1408  34047  bnj1450  34061  bnj1498  34072  bnj1514  34074  bnj1501  34078