Theorem bnj593 32725

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

Syntax hints:   → wi 4  ∃wex 1782

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

This theorem depends on definitions:  df-bi 206  df-ex 1783

This theorem is referenced by:  bnj1266  32791  bnj1304  32799  bnj1379  32810  bnj594  32892  bnj852  32901  bnj908  32911  bnj996  32936  bnj907  32947  bnj1128  32970  bnj1148  32976  bnj1154  32979  bnj1189  32989  bnj1245  32994  bnj1279  32998  bnj1286  32999  bnj1311  33004  bnj1371  33009  bnj1398  33014  bnj1408  33016  bnj1450  33030  bnj1498  33041  bnj1514  33043  bnj1501  33047