Theorem r19.29a 2999

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-12 1855

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1614  df-nf 1618  df-ral 2812  df-rex 2813

This theorem is referenced by:  xpdifid  5442  1arith  14457  ffthiso  15345  mhmid  16318  mhmmnd  16319  ghmgrp  16321  ghmcmn  16967  ablfac2  17267  zringlpirlem1  18636  zlpirlem1  18641  mp2pm2mplem4  19437  neiptopuni  19758  neiptoptop  19759  neiptopnei  19760  neitr  19808  hauscmplem  20033  2ndcomap  20085  lly1stc  20123  dissnref  20155  neitx  20234  cnextcn  20693  ustexsym  20844  ustex2sym  20845  ustex3sym  20846  trust  20858  utoptop  20863  restutop  20866  restutopopn  20867  ustuqtop1  20870  ustuqtop2  20871  ustuqtop3  20872  ustuqtop4  20873  utopreg  20881  ucncn  20914  fmucnd  20921  cfilufg  20922  trcfilu  20923  neipcfilu  20925  metustidOLD  21188  metustid  21189  metustsymOLD  21190  metustsym  21191  metustexhalfOLD  21192  metustexhalf  21193  metustOLD  21196  metust  21197  cfilucfilOLD  21198  cfilucfil  21199  metustblOLD  21209  metustbl  21210  metutopOLD  21211  psmetutop  21212  restmetu  21216  qdensere  21403  opnreen  21462  nmoleub2lem3  21724  ovolicc2lem4  22057  plydivlem4  22818  ulmuni  22913  dchrpt  23668  tgcgrtriv  24001  tgbtwntriv2  24004  tgbtwncom  24005  tgbtwnswapid  24009  tgbtwnintr  24010  tgbtwnouttr2  24012  tgtrisegint  24016  tgifscgr  24026  tgcgrxfr  24035  tgbtwnxfr  24044  motcgrg  24057  tgbtwnconn1lem3  24087  tgbtwnconn1  24088  tgbtwnconn3  24090  legval  24097  legov  24098  legov2  24099  legtrd  24102  legtri3  24103  legtrid  24104  ltgseg  24108  colline  24156  miriso  24176  symquadlem  24192  krippenlem  24193  midexlem  24195  perpneq  24217  isperp2  24218  footex  24221  perpdrag  24228  colperpexlem3  24232  colperpex  24233  opphllem  24235  mideulem  24236  midex  24237  oppnid  24244  opphllem3  24247  opphllem5  24249  opphllem6  24250  opphl  24251  hpgne1  24256  hpgne2  24257  lnopp2hpgb  24258  lmieu  24276  f1otrg  24301  ttgbtwnid  24314  cnvbraval  27156  opsqrlem1  27186  rabfodom  27532  acunirnmpt  27653  acunirnmpt2  27654  acunirnmpt2f  27655  xrge0infss  27737  archirngz  27893  archiabllem1a  27895  archiabllem1b  27896  archiabllem1  27897  archiabllem2a  27898  archiabllem2c  27899  archiabl  27902  gsummpt2d  27932  fimaproj  27997  txomap  27998  qtophaus  28000  pcmplfinf  28025  pstmxmet  28037  pnfneige0  28094  esumcst  28235  esum2d  28265  esumiun  28266  ddemeas  28381  signsply0  28705  signstres  28729  itg2gt0cn  30275  fdc1  30444  eldioph2b  30901  diophrex  30914  irrapxlem6  30967  pellex  30975  pellfundex  31026  lnrfg  31272  mpaaeu  31303  cvgdvgrat  31398  climsuse  31817  limsupre  31850  limcleqr  31853  cncficcgt0  31894  dvbdfbdioo  31930  ioodvbdlimc1lem2  31932  ioodvbdlimc2lem  31934  stoweidlem28  32013  stoweidlem29  32014  stoweidlem52  32037  stoweidlem60  32045  fourierdlem39  32131  fourierdlem102  32194  fourierdlem103  32195  fourierdlem104  32196  fourierdlem114  32206  lhprelat3N  35907  dihjat2  37301