Theorem bnj593 34908

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

Syntax hints:   → wi 4  ∃wex 1781

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

This theorem depends on definitions:  df-bi 207  df-ex 1782

This theorem is referenced by:  bnj1266  34973  bnj1304  34981  bnj1379  34992  bnj594  35074  bnj852  35083  bnj908  35093  bnj996  35118  bnj907  35129  bnj1128  35152  bnj1148  35158  bnj1154  35161  bnj1189  35171  bnj1245  35176  bnj1279  35180  bnj1286  35181  bnj1311  35186  bnj1371  35191  bnj1398  35196  bnj1408  35198  bnj1450  35212  bnj1498  35223  bnj1514  35225  bnj1501  35229