Theorem bnj593 30069

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

Syntax hints:   → wi 4  ∃wex 1695

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

This theorem depends on definitions:  df-bi 196  df-ex 1696

This theorem is referenced by:  bnj1266  30136  bnj1304  30144  bnj1379  30155  bnj594  30236  bnj852  30245  bnj908  30255  bnj996  30279  bnj907  30289  bnj1128  30312  bnj1148  30318  bnj1154  30321  bnj1189  30331  bnj1245  30336  bnj1279  30340  bnj1286  30341  bnj1311  30346  bnj1371  30351  bnj1398  30356  bnj1408  30358  bnj1450  30372  bnj1498  30383  bnj1514  30385  bnj1501  30389