Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  euan Structured version   Visualization version   Unicode version

Theorem euan 2379
 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
StepHypRef Expression
1 euex 2343 . . . 4
2 moanim.1 . . . . 5
3 simpl 464 . . . . 5
42, 3exlimi 2015 . . . 4
51, 4syl 17 . . 3
6 ibar 512 . . . . 5
72, 6eubid 2337 . . . 4
87biimprcd 233 . . 3
95, 8jcai 545 . 2
107biimpa 492 . 2
119, 10impbii 192 1
 Colors of variables: wff setvar class Syntax hints:   wb 189   wa 376  wex 1671  wnf 1675  weu 2319 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-12 1950 This theorem depends on definitions:  df-bi 190  df-an 378  df-ex 1672  df-nf 1676  df-eu 2323 This theorem is referenced by:  euanv  2383  2eu7  2408  2eu8  2409
 Copyright terms: Public domain W3C validator