This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem exan

Description: Place a conjunct in the scope of an existential quantifier. (Contributed by NM, 18-Aug-1993) (Proof shortened by Andrew Salmon, 25-May-2011) (Proof shortened by Wolf Lammen, 13-Jan-2018) Reduce axiom dependencies. (Revised by BJ, 7-Jul-2021) (Proof shortened by Wolf Lammen, 6-Nov-2022) Expand hypothesis. (Revised by Steven Nguyen, 19-Jun-2023)

	Ref	Expression
Hypotheses	exan.1	⊢ ∃ 𝑥 𝜑
	exan.2	⊢ 𝜓
Assertion	exan	⊢ ∃ 𝑥 ( 𝜑 ∧ 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		exan.1	⊢ ∃ 𝑥 𝜑
2		exan.2	⊢ 𝜓
3	2	jctr	⊢ ( 𝜑 → ( 𝜑 ∧ 𝜓 ) )
4	1 3	eximii	⊢ ∃ 𝑥 ( 𝜑 ∧ 𝜓 )