Theorem bnj593 30789

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

Syntax hints:   → wi 4  ∃wex 1702

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

This theorem depends on definitions:  df-bi 197  df-ex 1703

This theorem is referenced by:  bnj1266  30856  bnj1304  30864  bnj1379  30875  bnj594  30956  bnj852  30965  bnj908  30975  bnj996  30999  bnj907  31009  bnj1128  31032  bnj1148  31038  bnj1154  31041  bnj1189  31051  bnj1245  31056  bnj1279  31060  bnj1286  31061  bnj1311  31066  bnj1371  31071  bnj1398  31076  bnj1408  31078  bnj1450  31092  bnj1498  31103  bnj1514  31105  bnj1501  31109