Theorem moani 2581

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 2580	. 2 ⊢ (∃*𝑥𝜑 → ∃*𝑥(𝜓 ∧ 𝜑))
3	1, 2	ax-mp 5	1 ⊢ ∃*𝑥(𝜓 ∧ 𝜑)

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

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 1945  ax-6 2002  ax-7 2043

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

This theorem is used by:  euxfr2w  3681  euxfr2  3683  rmoeq  3699  reuxfrd  3709  fvopab6  7054  mpofun  7570  funmpt3  7714  mpt3fvd  7715  1stconst  8141  2ndconst  8142  pwfir  9339  iunmapdisj  10132  axaddf  11260  axmulf  11261  joinval  18581  meetval  18595  reuxfrdf  33162  mpofvd  35810