Theorem bnj593 34729

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  34795  bnj1304  34803  bnj1379  34814  bnj594  34896  bnj852  34905  bnj908  34915  bnj996  34940  bnj907  34951  bnj1128  34974  bnj1148  34980  bnj1154  34983  bnj1189  34993  bnj1245  34998  bnj1279  35002  bnj1286  35003  bnj1311  35008  bnj1371  35013  bnj1398  35018  bnj1408  35020  bnj1450  35034  bnj1498  35045  bnj1514  35047  bnj1501  35051