Theorem bnj1023

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bnj1023.1	⊢ ∃ 𝑥 ( 𝜑 → 𝜓 )
	bnj1023.2	⊢ ( 𝜓 → 𝜒 )
Assertion	bnj1023	⊢ ∃ 𝑥 ( 𝜑 → 𝜒 )

Proof

Step	Hyp	Ref	Expression
1		bnj1023.1	⊢ ∃ 𝑥 ( 𝜑 → 𝜓 )
2		bnj1023.2	⊢ ( 𝜓 → 𝜒 )
3	2	a1i	⊢ ( ( 𝜑 → 𝜓 ) → ( 𝜓 → 𝜒 ) )
4	3	ax-gen	⊢ ∀ 𝑥 ( ( 𝜑 → 𝜓 ) → ( 𝜓 → 𝜒 ) )
5		exintr	⊢ ( ∀ 𝑥 ( ( 𝜑 → 𝜓 ) → ( 𝜓 → 𝜒 ) ) → ( ∃ 𝑥 ( 𝜑 → 𝜓 ) → ∃ 𝑥 ( ( 𝜑 → 𝜓 ) ∧ ( 𝜓 → 𝜒 ) ) ) )
6	4 1 5	mp2	⊢ ∃ 𝑥 ( ( 𝜑 → 𝜓 ) ∧ ( 𝜓 → 𝜒 ) )
7		pm3.33	⊢ ( ( ( 𝜑 → 𝜓 ) ∧ ( 𝜓 → 𝜒 ) ) → ( 𝜑 → 𝜒 ) )
8	6 7	bnj101	⊢ ∃ 𝑥 ( 𝜑 → 𝜒 )