Theorem r19.29an 3077

Description: A commonly used pattern based on r19.29 3072. (Contributed by Thierry Arnoux, 29-Dec-2019.)

Hypothesis

Ref	Expression
r19.29an.1	|- ( ( ( ph /\ x e. A ) /\ ps ) -> ch )

Assertion

Ref	Expression
r19.29an	|- ( ( ph /\ E. x e. A ps ) -> ch )

Distinct variable groups:   ch, x   ph, x

Allowed substitution hints:   ps( x)   A( x)

Proof of Theorem r19.29an

Step	Hyp	Ref	Expression
1		nfv 1843	. . 3 |- F/ x ph
2		nfre1 3005	. . 3 |- F/ x E. x e. A ps
3	1, 2	nfan 1828	. 2 |- F/ x ( ph /\ E. x e. A ps )
4		r19.29an.1	. . 3 |- ( ( ( ph /\ x e. A ) /\ ps ) -> ch )
5	4	adantllr 755	. 2 |- ( ( ( ( ph /\ E. x e. A ps ) /\ x e. A ) /\ ps ) -> ch )
6		simpr 477	. 2 |- ( ( ph /\ E. x e. A ps ) -> E. x e. A ps )
7	3, 5, 6	r19.29af 3076	1 |- ( ( ph /\ E. x e. A ps ) -> ch )

Syntax hints:   -> wi 4   /\ wa 384   e. wcel 1990   E.wrex 2913

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-10 2019  ax-12 2047

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-ral 2917  df-rex 2918

This theorem is referenced by:  summolem2  14447  cygabl  18292  dissnlocfin  21332  utopsnneiplem  22051  restmetu  22375  elqaa  24077  colline  25544  f1otrg  25751  axcontlem2  25845  grpoidinvlem4  27361  2sqmo  29649  isarchi3  29741  fimaproj  29900  qtophaus  29903  locfinreflem  29907  cmpcref  29917  ordtconnlem1  29970  esumpcvgval  30140  esumcvg  30148  eulerpartlems  30422  eulerpartlemgvv  30438  reprinfz1  30700  reprpmtf1o  30704  isbnd3  33583  eldiophss  37338  eldioph4b  37375  pellfund14b  37463  opeoALTV  41595