Theorem exlimd 2087

Description: Deduction form of Theorem 19.9 of [Margaris] p. 89. (Contributed by NM, 23-Jan-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 12-Jan-2018.)

Hypotheses

Ref	Expression
exlimd.1	|- F/ x ph
exlimd.2	|- F/ x ch
exlimd.3	|- ( ph -> ( ps -> ch ) )

Assertion

Ref	Expression
exlimd	|- ( ph -> ( E. x ps -> ch ) )

Proof of Theorem exlimd

Step	Hyp	Ref	Expression
1		exlimd.1	. . 3 |- F/ x ph
2		exlimd.3	. . 3 |- ( ph -> ( ps -> ch ) )
3	1, 2	eximd 2085	. 2 |- ( ph -> ( E. x ps -> E. x ch ) )
4		exlimd.2	. . 3 |- F/ x ch
5	4	19.9 2072	. 2 |- ( E. x ch <-> ch )
6	3, 5	syl6ib 241	1 |- ( ph -> ( E. x ps -> ch ) )

Syntax hints:   -> wi 4   E.wex 1704   F/wnf 1708

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-12 2047

This theorem depends on definitions:  df-bi 197  df-ex 1705  df-nf 1710

This theorem is referenced by:  exlimdd  2088  exlimdh  2149  equs5  2351  moexex  2541  2eu6  2558  exists2  2562  ceqsalgALT  3231  alxfr  4878  copsex2t  4957  mosubopt  4972  ovmpt2df  6792  ov3  6797  tz7.48-1  7538  ac6c4  9303  fsum2dlem  14501  fprod2dlem  14710  gsum2d2lem  18372  padct  29497  exlimim  33189  exellim  33192  wl-lem-moexsb  33350  exlimddvf  33926  stoweidlem27  40244  fourierdlem31  40355  intsaluni  40547  isomenndlem  40744