Theorem bnj593 34738

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

Syntax hints:   → wi 4  ∃wex 1776

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

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

This theorem is referenced by:  bnj1266  34804  bnj1304  34812  bnj1379  34823  bnj594  34905  bnj852  34914  bnj908  34924  bnj996  34949  bnj907  34960  bnj1128  34983  bnj1148  34989  bnj1154  34992  bnj1189  35002  bnj1245  35007  bnj1279  35011  bnj1286  35012  bnj1311  35017  bnj1371  35022  bnj1398  35027  bnj1408  35029  bnj1450  35043  bnj1498  35054  bnj1514  35056  bnj1501  35060