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

Theorem r19.29_2a 3005
Description: A commonly used pattern based on r19.29 2997, version with two restricted quantifiers (Contributed by Thierry Arnoux, 26-Nov-2017.)
Hypotheses
Ref Expression
r19.29_2a.1  |-  ( ( ( ( ph  /\  x  e.  A )  /\  y  e.  B
)  /\  ps )  ->  ch )
r19.29_2a.2  |-  ( ph  ->  E. x  e.  A  E. y  e.  B  ps )
Assertion
Ref Expression
r19.29_2a  |-  ( 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.29_2a
StepHypRef Expression
1 r19.29_2a.1 . . . . . 6  |-  ( ( ( ( ph  /\  x  e.  A )  /\  y  e.  B
)  /\  ps )  ->  ch )
21ex 434 . . . . 5  |-  ( ( ( ph  /\  x  e.  A )  /\  y  e.  B )  ->  ( ps  ->  ch ) )
32ralrimiva 2878 . . . 4  |-  ( (
ph  /\  x  e.  A )  ->  A. y  e.  B  ( ps  ->  ch ) )
43ralrimiva 2878 . . 3  |-  ( ph  ->  A. x  e.  A  A. y  e.  B  ( ps  ->  ch )
)
5 r19.29_2a.2 . . 3  |-  ( ph  ->  E. x  e.  A  E. y  e.  B  ps )
64, 5r19.29d2r 3004 . 2  |-  ( ph  ->  E. x  e.  A  E. y  e.  B  ( ( ps  ->  ch )  /\  ps )
)
7 pm3.35 587 . . . . 5  |-  ( ( ps  /\  ( ps 
->  ch ) )  ->  ch )
87ancoms 453 . . . 4  |-  ( ( ( ps  ->  ch )  /\  ps )  ->  ch )
98rexlimivw 2952 . . 3  |-  ( E. y  e.  B  ( ( ps  ->  ch )  /\  ps )  ->  ch )
109rexlimivw 2952 . 2  |-  ( E. x  e.  A  E. y  e.  B  (
( ps  ->  ch )  /\  ps )  ->  ch )
116, 10syl 16 1  |-  ( ph  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1767   A.wral 2814   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
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-ral 2819  df-rex 2820
This theorem is referenced by:  trust  20495  utoptop  20500  metusttoOLD  20823  metustto  20824  restmetu  20853  tgbtwndiff  23653  legov  23727  legso  23740  tglnne  23750  tglndim0  23751  tglinethru  23758  tglnpt2  23762  footex  23831  mideu  23842  f1otrge  23879  archiabllem2c  27429  txomap  27528  pstmfval  27539  qtophaus  27665  eulerpartlemgvv  27983
  Copyright terms: Public domain W3C validator