Theorem bnj593 35296

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

This proof depends on syntax axioms:   → wi 4  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-ex 1813

This theorem is used by:  bnj1266  35361  bnj1304  35369  bnj1379  35380  bnj594  35462  bnj852  35471  bnj908  35481  bnj996  35506  bnj907  35517  bnj1128  35540  bnj1148  35546  bnj1154  35549  bnj1189  35559  bnj1245  35564  bnj1279  35568  bnj1286  35569  bnj1311  35574  bnj1371  35579  bnj1398  35584  bnj1408  35586  bnj1450  35600  bnj1498  35611  bnj1514  35613  bnj1501  35617