Theorem bnj593 31153

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

Syntax hints:   → wi 4  ∃wex 1852

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

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

This theorem is referenced by:  bnj1266  31220  bnj1304  31228  bnj1379  31239  bnj594  31320  bnj852  31329  bnj908  31339  bnj996  31363  bnj907  31373  bnj1128  31396  bnj1148  31402  bnj1154  31405  bnj1189  31415  bnj1245  31420  bnj1279  31424  bnj1286  31425  bnj1311  31430  bnj1371  31435  bnj1398  31440  bnj1408  31442  bnj1450  31456  bnj1498  31467  bnj1514  31469  bnj1501  31473