Theorem r19.29a 2857

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-12 1792

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-ral 2715  df-rex 2716

This theorem is referenced by:  xpdifid  5261  zringlpirlem1  17878  neiptopuni  18709  neiptoptop  18710  neiptopnei  18711  neitr  18759  neitx  19155  cnextcn  19614  ustexsym  19765  ustex2sym  19766  ustex3sym  19767  trust  19779  utoptop  19784  restutop  19787  restutopopn  19788  ustuqtop1  19791  ustuqtop2  19792  ustuqtop3  19793  ustuqtop4  19794  utopreg  19802  ucncn  19835  fmucnd  19842  cfilufg  19843  trcfilu  19844  neipcfilu  19846  metustidOLD  20109  metustid  20110  metustsymOLD  20111  metustsym  20112  metustexhalfOLD  20113  metustexhalf  20114  metustOLD  20117  metust  20118  cfilucfilOLD  20119  cfilucfil  20120  metustblOLD  20130  metustbl  20131  metutopOLD  20132  psmetutop  20133  restmetu  20137  ovolicc2lem4  20978  tgcgrtriv  22913  tgbtwntriv2  22916  tgbtwncom  22917  tgbtwnswapid  22920  tgbtwnintr  22921  tgbtwnouttr2  22923  tgtrisegint  22927  tgifscgr  22936  tgcgrxfr  22945  tgbtwnxfr  22954  tgbtwnconn1lem3  22977  tgbtwnconn1  22978  tgbtwnconn3  22980  legval  22986  legov  22987  legov2  22988  legtrd  22991  legtri3  22992  legtrid  22993  colline  23020  miriso  23039  symquadlem  23048  krippenlem  23049  midexlem  23051  f1otrg  23068  ttgbtwnid  23081  xrge0infss  26004  archirngz  26157  archiabllem1a  26159  archiabllem1b  26160  archiabllem1  26161  archiabllem2a  26162  archiabllem2c  26163  archiabl  26166  pstmxmet  26276  pnfneige0  26333  esumcst  26466  ddemeas  26604  signsply0  26904  signstres  26928  stoweidlem28  29776  stoweidlem29  29777  stoweidlem52  29800  stoweidlem60  29808