Theorem exsimpl 1461

Description: Simplification of an existentially quantified conjunction. (Contributed by Rodolfo Medina, 25-Sep-2010.) (The proof was shortened by Andrew Salmon, 29-Jun-2011.)

Assertion

Ref	Expression
exsimpl	|- (E.x(ph /\ ps) -> E.xph)

Proof of Theorem exsimpl

Step	Hyp	Ref	Expression
1		simpl 346	. 2 |- ((ph /\ ps) -> ph)
2	1	eximi 1387	1 |- (E.x(ph /\ ps) -> E.xph)

Syntax hints:   -> wi 3   /\ wa 240  E.wex 1326

This theorem is referenced by:  euex 1788  mopick2OLD 1838  moexex 1841  elisset 2299  r19.2zb 2959  dmcoss 4211  dmcosseqOLD 4215  unblem2 5634  kmlem8 5934  0re 6603  bnj1144 12941  bnj1237 13005  prtlem16 16272  pm10.55 16316

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-4 1319  ax-5o 1321

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327

Copyright terms: Public domain