Theorem r19.29a 3078

Description: A commonly used pattern based on r19.29 3072. (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 1843	. 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 3076	1 |- ( ph -> 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-12 2047

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

This theorem is referenced by:  xpdifid  5562  modmuladdnn0  12714  1arith  15631  prmgaplem5  15759  prmgapprmolem  15765  ffthiso  16589  mhmid  17536  mhmmnd  17537  ghmgrp  17539  ghmcmn  18237  ablfac2  18488  zringlpirlem1  19832  mp2pm2mplem4  20614  neiptopuni  20934  neiptoptop  20935  neiptopnei  20936  neitr  20984  hauscmplem  21209  2ndcomap  21261  lly1stc  21299  dissnref  21331  neitx  21410  cnextcn  21871  ustexsym  22019  ustex2sym  22020  ustex3sym  22021  trust  22033  utoptop  22038  restutop  22041  restutopopn  22042  ustuqtop1  22045  ustuqtop2  22046  ustuqtop3  22047  ustuqtop4  22048  utopreg  22056  ucncn  22089  fmucnd  22096  cfilufg  22097  trcfilu  22098  neipcfilu  22100  metustid  22359  metustsym  22360  metustexhalf  22361  metust  22363  cfilucfil  22364  metustbl  22371  psmetutop  22372  restmetu  22375  qdensere  22573  opnreen  22634  nmoleub2lem3  22915  ovolicc2lem4  23288  plydivlem4  24051  ulmuni  24146  dchrpt  24992  tgcgrtriv  25379  tgbtwntriv2  25382  tgbtwncom  25383  tgbtwnswapid  25387  tgbtwnintr  25388  tgbtwnouttr2  25390  tgtrisegint  25394  tgifscgr  25403  tgcgrxfr  25413  tgbtwnxfr  25425  motcgrg  25439  tgbtwnconn1lem3  25469  tgbtwnconn1  25470  tgbtwnconn3  25472  legval  25479  legov  25480  legov2  25481  legtrd  25484  legtri3  25485  legtrid  25486  ltgseg  25491  hlcgrex  25511  hlcgreulem  25512  colline  25544  miriso  25565  symquadlem  25584  krippenlem  25585  midexlem  25587  perpneq  25609  isperp2  25610  footex  25613  perpdrag  25620  colperpexlem3  25624  colperpex  25625  opphllem  25627  mideulem  25628  midex  25629  oppne3  25635  oppnid  25638  opphllem3  25641  opphllem5  25643  opphllem6  25644  oppperpex  25645  opphl  25646  outpasch  25647  hpgne1  25653  hpgne2  25654  lnopp2hpgb  25655  colopp  25661  lmieu  25676  lnperpex  25695  trgcopy  25696  trgcopyeulem  25697  acopy  25724  acopyeu  25725  inaghl  25731  cgrg3col4  25734  tgasa1  25739  f1otrg  25751  ttgbtwnid  25764  cnvbraval  28969  opsqrlem1  28999  rabfodom  29344  acunirnmpt  29459  acunirnmpt2  29460  acunirnmpt2f  29461  xrge0infss  29525  fsumiunle  29575  archirngz  29743  archiabllem1a  29745  archiabllem1b  29746  archiabllem1  29747  archiabllem2a  29748  archiabllem2c  29749  archiabl  29752  gsummpt2d  29781  fimaproj  29900  txomap  29901  qtophaus  29903  pcmplfinf  29928  pstmxmet  29940  pnfneige0  29997  esumcst  30125  esum2d  30155  esumiun  30156  ddemeas  30299  signsply0  30628  signstres  30652  prodfzo03  30681  actfunsnf1o  30682  actfunsnrndisj  30683  tgoldbachgt  30741  poimirlem17  33426  poimirlem20  33429  itg2gt0cn  33465  fdc1  33542  lhprelat3N  35326  dihjat2  36720  eldioph2b  37326  diophrex  37339  irrapxlem6  37391  pellex  37399  pellfundex  37450  lnrfg  37689  mpaaeu  37720  cvgdvgrat  38512  climsuse  39840  limsupre  39873  limcleqr  39876  xlimclim2lem  40065  climxlim2  40072  cncficcgt0  40101  dvbdfbdioo  40145  ioodvbdlimc1lem2  40147  ioodvbdlimc2lem  40149  stoweidlem28  40245  stoweidlem29  40246  stoweidlem52  40269  stoweidlem60  40277  fourierdlem39  40363  fourierdlem102  40425  fourierdlem103  40426  fourierdlem104  40427  fourierdlem114  40437  hspmbllem2  40841  nnsum4primesevenALTV  41689