Theorem bnj593 34735

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  34801  bnj1304  34809  bnj1379  34820  bnj594  34902  bnj852  34911  bnj908  34921  bnj996  34946  bnj907  34957  bnj1128  34980  bnj1148  34986  bnj1154  34989  bnj1189  34999  bnj1245  35004  bnj1279  35008  bnj1286  35009  bnj1311  35014  bnj1371  35019  bnj1398  35024  bnj1408  35026  bnj1450  35040  bnj1498  35051  bnj1514  35053  bnj1501  35057