Theorem bnj593 34728

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  34794  bnj1304  34802  bnj1379  34813  bnj594  34895  bnj852  34904  bnj908  34914  bnj996  34939  bnj907  34950  bnj1128  34973  bnj1148  34979  bnj1154  34982  bnj1189  34992  bnj1245  34997  bnj1279  35001  bnj1286  35002  bnj1311  35007  bnj1371  35012  bnj1398  35017  bnj1408  35019  bnj1450  35033  bnj1498  35044  bnj1514  35046  bnj1501  35050