Theorem bnj593 34757

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

Syntax hints:   → wi 4  ∃wex 1780

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

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

This theorem is referenced by:  bnj1266  34823  bnj1304  34831  bnj1379  34842  bnj594  34924  bnj852  34933  bnj908  34943  bnj996  34968  bnj907  34979  bnj1128  35002  bnj1148  35008  bnj1154  35011  bnj1189  35021  bnj1245  35026  bnj1279  35030  bnj1286  35031  bnj1311  35036  bnj1371  35041  bnj1398  35046  bnj1408  35048  bnj1450  35062  bnj1498  35073  bnj1514  35075  bnj1501  35079