Theorem r19.29a 2852

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-12 1791

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-ral 2710  df-rex 2711

This theorem is referenced by:  xpdifid  5254  zringlpirlem1  17745  neiptopuni  18576  neiptoptop  18577  neiptopnei  18578  neitr  18626  neitx  19022  cnextcn  19481  ustexsym  19632  ustex2sym  19633  ustex3sym  19634  trust  19646  utoptop  19651  restutop  19654  restutopopn  19655  ustuqtop1  19658  ustuqtop2  19659  ustuqtop3  19660  ustuqtop4  19661  utopreg  19669  ucncn  19702  fmucnd  19709  cfilufg  19710  trcfilu  19711  neipcfilu  19713  metustidOLD  19976  metustid  19977  metustsymOLD  19978  metustsym  19979  metustexhalfOLD  19980  metustexhalf  19981  metustOLD  19984  metust  19985  cfilucfilOLD  19986  cfilucfil  19987  metustblOLD  19997  metustbl  19998  metutopOLD  19999  psmetutop  20000  restmetu  20004  ovolicc2lem4  20845  tgcgrtriv  22820  tgbtwntriv2  22823  tgbtwncom  22824  tgbtwnswapid  22827  tgbtwnintr  22828  tgbtwnouttr2  22830  tgtrisegint  22834  tgifscgr  22842  tgcgrxfr  22851  tgbtwnxfr  22860  tgbtwnconn1lem3  22882  tgbtwnconn1  22883  tgbtwnconn3  22885  legval  22891  legov  22892  legov2  22893  legtrd  22896  legtri3  22897  legtrid  22898  colline  22918  miriso  22935  f1otrg  22940  ttgbtwnid  22953  archirngz  26030  archiabllem1a  26032  archiabllem1b  26033  archiabllem1  26034  archiabllem2a  26035  archiabllem2c  26036  archiabl  26039  pstmxmet  26178  pnfneige0  26235  esumcst  26368  ddemeas  26506  signsply0  26800  signstres  26824