Theorem bnj593 32018

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 1780

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

This theorem depends on definitions:  df-bi 209  df-ex 1781

This theorem is referenced by:  bnj1266  32085  bnj1304  32093  bnj1379  32104  bnj594  32186  bnj852  32195  bnj908  32205  bnj996  32230  bnj907  32241  bnj1128  32264  bnj1148  32270  bnj1154  32273  bnj1189  32283  bnj1245  32288  bnj1279  32292  bnj1286  32293  bnj1311  32298  bnj1371  32303  bnj1398  32308  bnj1408  32310  bnj1450  32324  bnj1498  32335  bnj1514  32337  bnj1501  32341