Theorem bnj593 32126

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 1781

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

This theorem depends on definitions:  df-bi 210  df-ex 1782

This theorem is referenced by:  bnj1266  32193  bnj1304  32201  bnj1379  32212  bnj594  32294  bnj852  32303  bnj908  32313  bnj996  32338  bnj907  32349  bnj1128  32372  bnj1148  32378  bnj1154  32381  bnj1189  32391  bnj1245  32396  bnj1279  32400  bnj1286  32401  bnj1311  32406  bnj1371  32411  bnj1398  32416  bnj1408  32418  bnj1450  32432  bnj1498  32443  bnj1514  32445  bnj1501  32449