Theorem r19.29a 2966

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-12 1794

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-nf 1591  df-ral 2803  df-rex 2804

This theorem is referenced by:  xpdifid  5373  zringlpirlem1  18027  neiptopuni  18865  neiptoptop  18866  neiptopnei  18867  neitr  18915  neitx  19311  cnextcn  19770  ustexsym  19921  ustex2sym  19922  ustex3sym  19923  trust  19935  utoptop  19940  restutop  19943  restutopopn  19944  ustuqtop1  19947  ustuqtop2  19948  ustuqtop3  19949  ustuqtop4  19950  utopreg  19958  ucncn  19991  fmucnd  19998  cfilufg  19999  trcfilu  20000  neipcfilu  20002  metustidOLD  20265  metustid  20266  metustsymOLD  20267  metustsym  20268  metustexhalfOLD  20269  metustexhalf  20270  metustOLD  20273  metust  20274  cfilucfilOLD  20275  cfilucfil  20276  metustblOLD  20286  metustbl  20287  metutopOLD  20288  psmetutop  20289  restmetu  20293  ovolicc2lem4  21134  tgcgrtriv  23071  tgbtwntriv2  23074  tgbtwncom  23075  tgbtwnswapid  23079  tgbtwnintr  23080  tgbtwnouttr2  23082  tgtrisegint  23086  tgifscgr  23096  tgcgrxfr  23105  tgbtwnxfr  23114  tgbtwnconn1lem3  23142  tgbtwnconn1  23143  tgbtwnconn3  23145  legval  23152  legov  23153  legov2  23154  legtrd  23157  legtri3  23158  legtrid  23159  colline  23193  miriso  23215  symquadlem  23225  krippenlem  23226  midexlem  23228  perpneq  23249  isperp2  23250  footex  23253  colperplem3  23258  colperp  23259  mideulem  23260  mideu  23261  f1otrg  23268  ttgbtwnid  23281  xrge0infss  26203  archirngz  26350  archiabllem1a  26352  archiabllem1b  26353  archiabllem1  26354  archiabllem2a  26355  archiabllem2c  26356  archiabl  26359  pstmxmet  26468  pnfneige0  26525  esumcst  26658  ddemeas  26795  signsply0  27095  signstres  27119  stoweidlem28  29970  stoweidlem29  29971  stoweidlem52  29994  stoweidlem60  30002  mp2pm2mplem4  31281