Theorem bnj593 32625

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 1783

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

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

This theorem is referenced by:  bnj1266  32691  bnj1304  32699  bnj1379  32710  bnj594  32792  bnj852  32801  bnj908  32811  bnj996  32836  bnj907  32847  bnj1128  32870  bnj1148  32876  bnj1154  32879  bnj1189  32889  bnj1245  32894  bnj1279  32898  bnj1286  32899  bnj1311  32904  bnj1371  32909  bnj1398  32914  bnj1408  32916  bnj1450  32930  bnj1498  32941  bnj1514  32943  bnj1501  32947