Theorem r19.29a 2918

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

Syntax hints:   -> wi 4   /\ wa 376   e. wcel 1904   E.wrex 2757

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-12 1950

This theorem depends on definitions:  df-bi 190  df-an 378  df-ex 1672  df-nf 1676  df-ral 2761  df-rex 2762

This theorem is referenced by:  xpdifid  5271  1arith  14950  prmgaplem5  15104  prmgapprmolem  15111  ffthiso  15912  mhmid  16885  mhmmnd  16886  ghmgrp  16888  ghmcmn  17550  ablfac2  17800  zringlpirlem1  19130  mp2pm2mplem4  19910  neiptopuni  20223  neiptoptop  20224  neiptopnei  20225  neitr  20273  hauscmplem  20498  2ndcomap  20550  lly1stc  20588  dissnref  20620  neitx  20699  cnextcn  21160  ustexsym  21308  ustex2sym  21309  ustex3sym  21310  trust  21322  utoptop  21327  restutop  21330  restutopopn  21331  ustuqtop1  21334  ustuqtop2  21335  ustuqtop3  21336  ustuqtop4  21337  utopreg  21345  ucncn  21378  fmucnd  21385  cfilufg  21386  trcfilu  21387  neipcfilu  21389  metustid  21647  metustsym  21648  metustexhalf  21649  metust  21651  cfilucfil  21652  metustbl  21659  psmetutop  21660  restmetu  21663  qdensere  21868  opnreen  21927  nmoleub2lem3  22207  ovolicc2lem4OLD  22551  ovolicc2lem4  22552  plydivlem4  23328  ulmuni  23426  dchrpt  24274  tgcgrtriv  24607  tgbtwntriv2  24610  tgbtwncom  24611  tgbtwnswapid  24615  tgbtwnintr  24616  tgbtwnouttr2  24618  tgtrisegint  24622  tgifscgr  24632  tgcgrxfr  24642  tgbtwnxfr  24654  motcgrg  24668  tgbtwnconn1lem3  24698  tgbtwnconn1  24699  tgbtwnconn3  24701  legval  24708  legov  24709  legov2  24710  legtrd  24713  legtri3  24714  legtrid  24715  ltgseg  24720  hlcgrex  24740  hlcgreulem  24741  colline  24773  miriso  24794  symquadlem  24813  krippenlem  24814  midexlem  24816  perpneq  24838  isperp2  24839  footex  24842  perpdrag  24849  colperpexlem3  24853  colperpex  24854  opphllem  24856  mideulem  24857  midex  24858  oppne3  24864  oppnid  24867  opphllem3  24870  opphllem5  24872  opphllem6  24873  oppperpex  24874  opphl  24875  outpasch  24876  hpgne1  24882  hpgne2  24883  lnopp2hpgb  24884  colopp  24890  lmieu  24905  lnperpex  24924  trgcopy  24925  trgcopyeulem  24926  acopy  24953  acopyeu  24954  inaghl  24960  cgrg3col4  24963  tgasa1  24968  f1otrg  24980  ttgbtwnid  24993  cnvbraval  27844  opsqrlem1  27874  rabfodom  28219  acunirnmpt  28336  acunirnmpt2  28337  acunirnmpt2f  28338  xrge0infss  28415  xrge0infssOLD  28416  archirngz  28580  archiabllem1a  28582  archiabllem1b  28583  archiabllem1  28584  archiabllem2a  28585  archiabllem2c  28586  archiabl  28589  gsummpt2d  28618  fimaproj  28734  txomap  28735  qtophaus  28737  pcmplfinf  28762  pstmxmet  28774  pnfneige0  28831  esumcst  28958  esum2d  28988  esumiun  28989  ddemeas  29132  signsply0  29512  signstres  29536  poimirlem17  32021  poimirlem20  32024  itg2gt0cn  32061  fdc1  32139  lhprelat3N  33676  dihjat2  35070  eldioph2b  35676  diophrex  35689  irrapxlem6  35742  pellex  35750  pellfundex  35805  lnrfg  36049  mpaaeu  36087  cvgdvgrat  36732  climsuse  37784  limsupre  37818  limsupreOLD  37819  limcleqr  37822  cncficcgt0  37863  dvbdfbdioo  37899  ioodvbdlimc1lem2  37901  ioodvbdlimc1lem2OLD  37903  ioodvbdlimc2lem  37905  ioodvbdlimc2lemOLD  37906  stoweidlem28  38000  stoweidlem29  38001  stoweidlem29OLD  38002  stoweidlem52  38025  stoweidlem60  38033  fourierdlem39  38121  fourierdlem102  38184  fourierdlem103  38185  fourierdlem104  38186  fourierdlem114  38196  hspmbllem2  38567  nnsum4primesevenALTV  39041