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

Theorem r19.29af 3001
Description: A commonly used pattern based on r19.29 2997 (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 1683 . 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 3000 1  |-  ( ph  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369   F/wnf 1599    e. wcel 1767   E.wrex 2815
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-12 1803
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-nf 1600  df-ral 2819  df-rex 2820
This theorem is referenced by:  r19.29an  3002  r19.29a  3003  neiptopnei  19427  neitr  19475  utopsnneiplem  20513  isucn2  20545  restmetu  20853  colline  23771  f1otrg  23878  isarchi3  27421  ordtconlem1  27570  oms0  27934  eulerpartlemgvv  27983  stoweidlem27  31355  stoweidlem35  31363
  Copyright terms: Public domain W3C validator