MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  r19.29an Structured version   Unicode version

Theorem r19.29an 2923
Description: A commonly used pattern based on r19.29 2917. (Contributed by Thierry Arnoux, 29-Dec-2019.)
Hypothesis
Ref Expression
r19.29an.1  |-  ( ( ( ph  /\  x  e.  A )  /\  ps )  ->  ch )
Assertion
Ref Expression
r19.29an  |-  ( (
ph  /\  E. x  e.  A  ps )  ->  ch )
Distinct variable groups:    ch, x    ph, x
Allowed substitution hints:    ps( x)    A( x)

Proof of Theorem r19.29an
StepHypRef Expression
1 nfv 1715 . . 3  |-  F/ x ph
2 nfre1 2843 . . 3  |-  F/ x E. x  e.  A  ps
31, 2nfan 1936 . 2  |-  F/ x
( ph  /\  E. x  e.  A  ps )
4 r19.29an.1 . . 3  |-  ( ( ( ph  /\  x  e.  A )  /\  ps )  ->  ch )
54adantllr 716 . 2  |-  ( ( ( ( ph  /\  E. x  e.  A  ps )  /\  x  e.  A
)  /\  ps )  ->  ch )
6 simpr 459 . 2  |-  ( (
ph  /\  E. x  e.  A  ps )  ->  E. x  e.  A  ps )
73, 5, 6r19.29af 2922 1  |-  ( (
ph  /\  E. x  e.  A  ps )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    e. wcel 1826   E.wrex 2733
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-12 1862
This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1621  df-nf 1625  df-ral 2737  df-rex 2738
This theorem is referenced by:  summolem2  13540  cygabl  17010  dissnlocfin  20115  utopsnneiplem  20835  restmetu  21175  elqaa  22803  colline  24150  f1otrg  24295  axcontlem2  24389  grpoidinvlem4  25326  2sqmo  27790  isarchi3  27884  fimaproj  27990  qtophaus  27993  locfinreflem  27997  cmpcref  28007  ordtconlem1  28060  esumpcvgval  28226  esumcvg  28234  eulerpartlems  28482  eulerpartlemgvv  28498  isbnd3  30446  eldiophss  30873  eldioph4b  30910  pellfund14b  31000  opeoALTV  32526
  Copyright terms: Public domain W3C validator