Theorem euan 2351

Description: Introduction of a conjunct into uniqueness quantifier. (Contributed by NM, 19-Feb-2005.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) (Proof shortened by Wolf Lammen, 24-Dec-2018.)

Hypothesis

Ref	Expression
moanim.1

Assertion

Ref	Expression
euan

Proof of Theorem euan

Step	Hyp	Ref	Expression
1		euex 2308	. . . 4
2		moanim.1	. . . . 5
3		simpl 457	. . . . 5
4	2, 3	exlimi 1912	. . . 4
5	1, 4	syl 16	. . 3
6		ibar 504	. . . . 5
7	2, 6	eubid 2302	. . . 4
8	7	biimprcd 225	. . 3
9	5, 8	jcai 536	. 2
10	7	biimpa 484	. 2
11	9, 10	impbii 188	1

Syntax hints:  <->wb 184  /\wa 369  E.wex 1612  F/wnf 1616  E!weu 2282

This theorem is referenced by:  euanv  2355  2eu7  2385  2eu8  2386

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-12 1854

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-nf 1617  df-eu 2286