Theorem r19.29a 3003

Description: A commonly used pattern based on r19.29 2997 (Contributed by Thierry Arnoux, 22-Nov-2017.)

Hypotheses

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

Assertion

Ref	Expression
r19.29a	|- ( ph -> ch )

Distinct variable groups:   ch, x   ph, x

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

Proof of Theorem r19.29a

Step	Hyp	Ref	Expression
1		nfv 1683	. 2 |- F/ x ph
2		r19.29a.1	. 2 |- ( ( ( ph /\ x e. A ) /\ ps ) -> ch )
3		r19.29a.2	. 2 |- ( ph -> E. x e. A ps )
4	1, 2, 3	r19.29af 3001	1 |- ( ph -> ch )

Syntax hints:   -> wi 4   /\ wa 369   e. wcel 1767   E.wrex 2815

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-12 1803

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-nf 1600  df-ral 2819  df-rex 2820

This theorem is referenced by:  xpdifid  5433  zringlpirlem1  18276  mp2pm2mplem4  19077  neiptopuni  19397  neiptoptop  19398  neiptopnei  19399  neitr  19447  neitx  19843  cnextcn  20302  ustexsym  20453  ustex2sym  20454  ustex3sym  20455  trust  20467  utoptop  20472  restutop  20475  restutopopn  20476  ustuqtop1  20479  ustuqtop2  20480  ustuqtop3  20481  ustuqtop4  20482  utopreg  20490  ucncn  20523  fmucnd  20530  cfilufg  20531  trcfilu  20532  neipcfilu  20534  metustidOLD  20797  metustid  20798  metustsymOLD  20799  metustsym  20800  metustexhalfOLD  20801  metustexhalf  20802  metustOLD  20805  metust  20806  cfilucfilOLD  20807  cfilucfil  20808  metustblOLD  20818  metustbl  20819  metutopOLD  20820  psmetutop  20821  restmetu  20825  ovolicc2lem4  21666  tgcgrtriv  23603  tgbtwntriv2  23606  tgbtwncom  23607  tgbtwnswapid  23611  tgbtwnintr  23612  tgbtwnouttr2  23614  tgtrisegint  23618  tgifscgr  23628  tgcgrxfr  23637  tgbtwnxfr  23646  motcgrg  23659  tgbtwnconn1lem3  23688  tgbtwnconn1  23689  tgbtwnconn3  23691  legval  23698  legov  23699  legov2  23700  legtrd  23703  legtri3  23704  legtrid  23705  ltgseg  23709  colline  23743  miriso  23763  symquadlem  23774  krippenlem  23775  midexlem  23777  perpneq  23799  isperp2  23800  footex  23803  perpdrag  23807  colperpexlem3  23811  colperpex  23812  mideulem  23813  mideu  23814  lmieu  23827  f1otrg  23850  ttgbtwnid  23863  xrge0infss  27248  archirngz  27395  archiabllem1a  27397  archiabllem1b  27398  archiabllem1  27399  archiabllem2a  27400  archiabllem2c  27401  archiabl  27404  fimaproj  27499  txomap  27500  pstmxmet  27512  pnfneige0  27569  qtophaus  27637  esumcst  27711  ddemeas  27848  signsply0  28148  signstres  28172  stoweidlem28  31328  stoweidlem29  31329  stoweidlem52  31352  stoweidlem60  31360