Theorem bnj593 31120

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

Syntax hints:   → wi 4  ∃wex 1851

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

This theorem depends on definitions:  df-bi 197  df-ex 1852

This theorem is referenced by:  bnj1266  31187  bnj1304  31195  bnj1379  31206  bnj594  31287  bnj852  31296  bnj908  31306  bnj996  31330  bnj907  31340  bnj1128  31363  bnj1148  31369  bnj1154  31372  bnj1189  31382  bnj1245  31387  bnj1279  31391  bnj1286  31392  bnj1311  31397  bnj1371  31402  bnj1398  31407  bnj1408  31409  bnj1450  31423  bnj1498  31434  bnj1514  31436  bnj1501  31440