Theorem bnj593 35079

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

Syntax hints:   → wi 4  ∃wex 1806

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

This theorem depends on definitions:  df-bi 210  df-ex 1807

This theorem is referenced by:  bnj1266  35144  bnj1304  35152  bnj1379  35163  bnj594  35245  bnj852  35254  bnj908  35264  bnj996  35289  bnj907  35300  bnj1128  35323  bnj1148  35329  bnj1154  35332  bnj1189  35342  bnj1245  35347  bnj1279  35351  bnj1286  35352  bnj1311  35357  bnj1371  35362  bnj1398  35367  bnj1408  35369  bnj1450  35383  bnj1498  35394  bnj1514  35396  bnj1501  35400