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

Theorem r19.29vva 2946
Description: A commonly used pattern based on r19.29 2937, version with two restricted quantifiers. (Contributed by Thierry Arnoux, 26-Nov-2017.)
Hypotheses
Ref Expression
r19.29vva.1  |-  ( ( ( ( ph  /\  x  e.  A )  /\  y  e.  B
)  /\  ps )  ->  ch )
r19.29vva.2  |-  ( ph  ->  E. x  e.  A  E. y  e.  B  ps )
Assertion
Ref Expression
r19.29vva  |-  ( ph  ->  ch )
Distinct variable groups:    y, A    x, y, ch    ph, x, y
Allowed substitution hints:    ps( x, y)    A( x)    B( x, y)

Proof of Theorem r19.29vva
StepHypRef Expression
1 r19.29vva.1 . . . . . 6  |-  ( ( ( ( ph  /\  x  e.  A )  /\  y  e.  B
)  /\  ps )  ->  ch )
21ex 440 . . . . 5  |-  ( ( ( ph  /\  x  e.  A )  /\  y  e.  B )  ->  ( ps  ->  ch ) )
32ralrimiva 2814 . . . 4  |-  ( (
ph  /\  x  e.  A )  ->  A. y  e.  B  ( ps  ->  ch ) )
43ralrimiva 2814 . . 3  |-  ( ph  ->  A. x  e.  A  A. y  e.  B  ( ps  ->  ch )
)
5 r19.29vva.2 . . 3  |-  ( ph  ->  E. x  e.  A  E. y  e.  B  ps )
64, 5r19.29d2r 2945 . 2  |-  ( ph  ->  E. x  e.  A  E. y  e.  B  ( ( ps  ->  ch )  /\  ps )
)
7 pm3.35 595 . . . . 5  |-  ( ( ps  /\  ( ps 
->  ch ) )  ->  ch )
87ancoms 459 . . . 4  |-  ( ( ( ps  ->  ch )  /\  ps )  ->  ch )
98rexlimivw 2888 . . 3  |-  ( E. y  e.  B  ( ( ps  ->  ch )  /\  ps )  ->  ch )
109rexlimivw 2888 . 2  |-  ( E. x  e.  A  E. y  e.  B  (
( ps  ->  ch )  /\  ps )  ->  ch )
116, 10syl 17 1  |-  ( ph  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375    e. wcel 1898   A.wral 2749   E.wrex 2750
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769
This theorem depends on definitions:  df-bi 190  df-an 377  df-ex 1675  df-ral 2754  df-rex 2755
This theorem is referenced by:  trust  21299  utoptop  21304  metustto  21623  restmetu  21640  tgbtwndiff  24606  legov  24686  legso  24700  tglnne  24729  tglndim0  24730  tglinethru  24737  tglnne0  24741  tglnpt2  24742  footex  24819  midex  24835  opptgdim2  24843  cgrane1  24910  cgrane2  24911  cgrane3  24912  cgrane4  24913  cgrahl1  24914  cgrahl2  24915  cgracgr  24916  cgratr  24921  cgrabtwn  24923  cgrahl  24924  dfcgra2  24927  sacgr  24928  acopyeu  24931  f1otrge  24958  archiabllem2c  28563  txomap  28712  qtophaus  28714  pstmfval  28750  eulerpartlemgvv  29259  irrapxlem4  35715
  Copyright terms: Public domain W3C validator