Theorem r19.29a 2970

Description: A commonly used pattern based on r19.29 2963. (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 1751	. 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 2968	1 |- ( ph -> ch )

Syntax hints:   -> wi 4   /\ wa 370   e. wcel 1868   E.wrex 2776

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-12 1905

This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1660  df-nf 1664  df-ral 2780  df-rex 2781

This theorem is referenced by:  xpdifid  5280  1arith  14858  prmgaplem5  15012  prmgapprmolem  15019  ffthiso  15821  mhmid  16794  mhmmnd  16795  ghmgrp  16797  ghmcmn  17459  ablfac2  17709  zringlpirlem1  19039  mp2pm2mplem4  19819  neiptopuni  20132  neiptoptop  20133  neiptopnei  20134  neitr  20182  hauscmplem  20407  2ndcomap  20459  lly1stc  20497  dissnref  20529  neitx  20608  cnextcn  21068  ustexsym  21216  ustex2sym  21217  ustex3sym  21218  trust  21230  utoptop  21235  restutop  21238  restutopopn  21239  ustuqtop1  21242  ustuqtop2  21243  ustuqtop3  21244  ustuqtop4  21245  utopreg  21253  ucncn  21286  fmucnd  21293  cfilufg  21294  trcfilu  21295  neipcfilu  21297  metustid  21555  metustsym  21556  metustexhalf  21557  metust  21559  cfilucfil  21560  metustbl  21567  psmetutop  21568  restmetu  21571  qdensere  21776  opnreen  21835  nmoleub2lem3  22115  ovolicc2lem4OLD  22459  ovolicc2lem4  22460  plydivlem4  23235  ulmuni  23333  dchrpt  24181  tgcgrtriv  24514  tgbtwntriv2  24517  tgbtwncom  24518  tgbtwnswapid  24522  tgbtwnintr  24523  tgbtwnouttr2  24525  tgtrisegint  24529  tgifscgr  24539  tgcgrxfr  24549  tgbtwnxfr  24561  motcgrg  24575  tgbtwnconn1lem3  24605  tgbtwnconn1  24606  tgbtwnconn3  24608  legval  24615  legov  24616  legov2  24617  legtrd  24620  legtri3  24621  legtrid  24622  ltgseg  24627  hlcgrex  24647  hlcgreulem  24648  colline  24680  miriso  24701  symquadlem  24720  krippenlem  24721  midexlem  24723  perpneq  24745  isperp2  24746  footex  24749  perpdrag  24756  colperpexlem3  24760  colperpex  24761  opphllem  24763  mideulem  24764  midex  24765  oppne3  24771  oppnid  24774  opphllem3  24777  opphllem5  24779  opphllem6  24780  oppperpex  24781  opphl  24782  outpasch  24783  hpgne1  24789  hpgne2  24790  lnopp2hpgb  24791  colopp  24797  lmieu  24812  lnperpex  24831  trgcopy  24832  trgcopyeulem  24833  acopy  24860  acopyeu  24861  inaghl  24867  cgrg3col4  24870  tgasa1  24875  f1otrg  24887  ttgbtwnid  24900  cnvbraval  27748  opsqrlem1  27778  rabfodom  28126  acunirnmpt  28250  acunirnmpt2  28251  acunirnmpt2f  28252  xrge0infss  28333  xrge0infssOLD  28334  archirngz  28500  archiabllem1a  28502  archiabllem1b  28503  archiabllem1  28504  archiabllem2a  28505  archiabllem2c  28506  archiabl  28509  gsummpt2d  28538  fimaproj  28655  txomap  28656  qtophaus  28658  pcmplfinf  28683  pstmxmet  28695  pnfneige0  28752  esumcst  28879  esum2d  28909  esumiun  28910  ddemeas  29054  signsply0  29435  signstres  29459  poimirlem17  31870  poimirlem20  31873  itg2gt0cn  31910  fdc1  31988  lhprelat3N  33523  dihjat2  34917  eldioph2b  35523  diophrex  35536  irrapxlem6  35590  pellex  35598  pellfundex  35653  lnrfg  35897  mpaaeu  35935  cvgdvgrat  36519  climsuse  37506  limsupre  37540  limsupreOLD  37541  limcleqr  37544  cncficcgt0  37585  dvbdfbdioo  37621  ioodvbdlimc1lem2  37623  ioodvbdlimc1lem2OLD  37625  ioodvbdlimc2lem  37627  ioodvbdlimc2lemOLD  37628  stoweidlem28  37707  stoweidlem29  37708  stoweidlem29OLD  37709  stoweidlem52  37732  stoweidlem60  37740  fourierdlem39  37828  fourierdlem102  37891  fourierdlem103  37892  fourierdlem104  37893  fourierdlem114  37903  nnsum4primesevenALTV  38607