Theorem bnj593 35376

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

This proof depends on syntax axioms:   → wi 4  ∃wex 1811

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841

This proof depends on definitions:  df-bi 210  df-ex 1812

This theorem is used by:  bnj1266  35441  bnj1304  35449  bnj1379  35460  bnj594  35542  bnj852  35551  bnj908  35561  bnj996  35586  bnj907  35597  bnj1128  35620  bnj1148  35626  bnj1154  35629  bnj1189  35639  bnj1245  35644  bnj1279  35648  bnj1286  35649  bnj1311  35654  bnj1371  35659  bnj1398  35664  bnj1408  35666  bnj1450  35680  bnj1498  35691  bnj1514  35693  bnj1501  35697