Theorem bnj593 34781

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

Syntax hints:   → wi 4  ∃wex 1779

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

This theorem depends on definitions:  df-bi 207  df-ex 1780

This theorem is referenced by:  bnj1266  34847  bnj1304  34855  bnj1379  34866  bnj594  34948  bnj852  34957  bnj908  34967  bnj996  34992  bnj907  35003  bnj1128  35026  bnj1148  35032  bnj1154  35035  bnj1189  35045  bnj1245  35050  bnj1279  35054  bnj1286  35055  bnj1311  35060  bnj1371  35065  bnj1398  35070  bnj1408  35072  bnj1450  35086  bnj1498  35097  bnj1514  35099  bnj1501  35103