Theorem moani 2579

Description: "At most one" is still true when a conjunct is added, inference form. (Contributed by NM, 9-Mar-1995.)

Hypothesis

Ref	Expression
moani.1	⊢ ∃*𝑥𝜑

Assertion

Ref	Expression
moani	⊢ ∃*𝑥(𝜓 ∧ 𝜑)

Proof of Theorem moani

Step	Hyp	Ref	Expression
1		moani.1	. 2 ⊢ ∃*𝑥𝜑
2		moan 2578	. 2 ⊢ (∃*𝑥𝜑 → ∃*𝑥(𝜓 ∧ 𝜑))
3	1, 2	ax-mp 5	1 ⊢ ∃*𝑥(𝜓 ∧ 𝜑)

This proof depends on syntax axioms:   ∧ wa 401  ∃*wmo 2563

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

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-mo 2565

This theorem is used by:  euxfr2w  3678  euxfr2  3680  rmoeq  3696  reuxfrd  3706  fvopab6  7020  mpofun  7536  funmpt3  7679  1stconst  8100  2ndconst  8101  pwfir  9292  iunmapdisj  10083  axaddf  11211  axmulf  11212  joinval  18529  meetval  18543  reuxfrdf  33069