Theorem r19.29a 2932

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

Syntax hints:   -> wi 4   /\ wa 371   e. wcel 1887   E.wrex 2738

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-12 1933

This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1664  df-nf 1668  df-ral 2742  df-rex 2743

This theorem is referenced by:  xpdifid  5265  1arith  14871  prmgaplem5  15025  prmgapprmolem  15032  ffthiso  15834  mhmid  16807  mhmmnd  16808  ghmgrp  16810  ghmcmn  17472  ablfac2  17722  zringlpirlem1  19053  mp2pm2mplem4  19833  neiptopuni  20146  neiptoptop  20147  neiptopnei  20148  neitr  20196  hauscmplem  20421  2ndcomap  20473  lly1stc  20511  dissnref  20543  neitx  20622  cnextcn  21082  ustexsym  21230  ustex2sym  21231  ustex3sym  21232  trust  21244  utoptop  21249  restutop  21252  restutopopn  21253  ustuqtop1  21256  ustuqtop2  21257  ustuqtop3  21258  ustuqtop4  21259  utopreg  21267  ucncn  21300  fmucnd  21307  cfilufg  21308  trcfilu  21309  neipcfilu  21311  metustid  21569  metustsym  21570  metustexhalf  21571  metust  21573  cfilucfil  21574  metustbl  21581  psmetutop  21582  restmetu  21585  qdensere  21790  opnreen  21849  nmoleub2lem3  22129  ovolicc2lem4OLD  22473  ovolicc2lem4  22474  plydivlem4  23249  ulmuni  23347  dchrpt  24195  tgcgrtriv  24528  tgbtwntriv2  24531  tgbtwncom  24532  tgbtwnswapid  24536  tgbtwnintr  24537  tgbtwnouttr2  24539  tgtrisegint  24543  tgifscgr  24553  tgcgrxfr  24563  tgbtwnxfr  24575  motcgrg  24589  tgbtwnconn1lem3  24619  tgbtwnconn1  24620  tgbtwnconn3  24622  legval  24629  legov  24630  legov2  24631  legtrd  24634  legtri3  24635  legtrid  24636  ltgseg  24641  hlcgrex  24661  hlcgreulem  24662  colline  24694  miriso  24715  symquadlem  24734  krippenlem  24735  midexlem  24737  perpneq  24759  isperp2  24760  footex  24763  perpdrag  24770  colperpexlem3  24774  colperpex  24775  opphllem  24777  mideulem  24778  midex  24779  oppne3  24785  oppnid  24788  opphllem3  24791  opphllem5  24793  opphllem6  24794  oppperpex  24795  opphl  24796  outpasch  24797  hpgne1  24803  hpgne2  24804  lnopp2hpgb  24805  colopp  24811  lmieu  24826  lnperpex  24845  trgcopy  24846  trgcopyeulem  24847  acopy  24874  acopyeu  24875  inaghl  24881  cgrg3col4  24884  tgasa1  24889  f1otrg  24901  ttgbtwnid  24914  cnvbraval  27763  opsqrlem1  27793  rabfodom  28140  acunirnmpt  28261  acunirnmpt2  28262  acunirnmpt2f  28263  xrge0infss  28340  xrge0infssOLD  28341  archirngz  28506  archiabllem1a  28508  archiabllem1b  28509  archiabllem1  28510  archiabllem2a  28511  archiabllem2c  28512  archiabl  28515  gsummpt2d  28544  fimaproj  28660  txomap  28661  qtophaus  28663  pcmplfinf  28688  pstmxmet  28700  pnfneige0  28757  esumcst  28884  esum2d  28914  esumiun  28915  ddemeas  29059  signsply0  29440  signstres  29464  poimirlem17  31957  poimirlem20  31960  itg2gt0cn  31997  fdc1  32075  lhprelat3N  33605  dihjat2  34999  eldioph2b  35605  diophrex  35618  irrapxlem6  35671  pellex  35679  pellfundex  35734  lnrfg  35978  mpaaeu  36016  cvgdvgrat  36662  climsuse  37687  limsupre  37721  limsupreOLD  37722  limcleqr  37725  cncficcgt0  37766  dvbdfbdioo  37802  ioodvbdlimc1lem2  37804  ioodvbdlimc1lem2OLD  37806  ioodvbdlimc2lem  37808  ioodvbdlimc2lemOLD  37809  stoweidlem28  37888  stoweidlem29  37889  stoweidlem29OLD  37890  stoweidlem52  37913  stoweidlem60  37921  fourierdlem39  38009  fourierdlem102  38072  fourierdlem103  38073  fourierdlem104  38074  fourierdlem114  38084  hspmbllem2  38449  nnsum4primesevenALTV  38896