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
r19.29_2a.2
Assertion
Ref Expression
r19.29_2a
Distinct variable groups:   ,   ,,   ,,
Allowed substitution hints:   (,)   ()   (,)

Proof of Theorem r19.29_2a
StepHypRef Expression
1 r19.29_2a.1 . . . . . 6
21ex 434 . . . . 5
32ralrimiva 2878 . . . 4
43ralrimiva 2878 . . 3
5 r19.29_2a.2 . . 3
64, 5r19.29d2r 3004 . 2
7 pm3.35 587 . . . . 5
87ancoms 453 . . . 4
98rexlimivw 2952 . . 3
109rexlimivw 2952 . 2
116, 10syl 16 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 369   wcel 1767  wral 2814  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