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 2864
Description: A commonly used pattern based on r19.29 2857, 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 2799 . . . 4  |-  ( (
ph  /\  x  e.  A )  ->  A. y  e.  B  ( ps  ->  ch ) )
43ralrimiva 2799 . . 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 2863 . 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 2837 . . 3  |-  ( E. y  e.  B  ( ( ps  ->  ch )  /\  ps )  ->  ch )
109rexlimivw 2837 . 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 1756   A.wral 2715   E.wrex 2716
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-12 1792
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-ral 2720  df-rex 2721
This theorem is referenced by:  trust  19804  utoptop  19809  metusttoOLD  20132  metustto  20133  restmetu  20162  tgbtwndiff  22959  legov  23016  tglndim0  23035  tglinethru  23042  tglnpt2  23046  footex  23109  f1otrge  23118  archiabllem2c  26212  pstmfval  26323  eulerpartlemgvv  26759
  Copyright terms: Public domain W3C validator