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

Theorem r19.29af 2997
Description: A commonly used pattern based on r19.29 2992. (Contributed by Thierry Arnoux, 29-Nov-2017.)
Hypotheses
Ref Expression
r19.29af.0  |-  F/ x ph
r19.29af.1  |-  ( ( ( ph  /\  x  e.  A )  /\  ps )  ->  ch )
r19.29af.2  |-  ( ph  ->  E. x  e.  A  ps )
Assertion
Ref Expression
r19.29af  |-  ( ph  ->  ch )
Distinct variable group:    ch, x
Allowed substitution hints:    ph( x)    ps( x)    A( x)

Proof of Theorem r19.29af
StepHypRef Expression
1 r19.29af.0 . 2  |-  F/ x ph
2 nfv 1708 . 2  |-  F/ x ch
3 r19.29af.1 . 2  |-  ( ( ( ph  /\  x  e.  A )  /\  ps )  ->  ch )
4 r19.29af.2 . 2  |-  ( ph  ->  E. x  e.  A  ps )
51, 2, 3, 4r19.29af2 2995 1  |-  ( ph  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369   F/wnf 1617    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:  r19.29an  2998  r19.29a  2999  neiptopnei  19759  neitr  19807  utopsnneiplem  20875  isucn2  20907  foresf1o  27530  elsnxp  27607  2sqmo  27789  reff  27995  locfinreflem  27996  ordtconlem1  28059  esum2dlem  28252  esum2d  28253  esumiun  28254  oms0  28429  eulerpartlemgvv  28490  stoweidlem27  31970  stoweidlem35  31978
  Copyright terms: Public domain W3C validator