Theorem r19.29_2a 3001

Description: A commonly used pattern based on r19.29 2992, 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:   ,   ,,   ,,

Proof of Theorem r19.29_2a

Step	Hyp	Ref	Expression
1		r19.29_2a.1	. . . . . 6
2	1	ex 434	. . . . 5
3	2	ralrimiva 2871	. . . 4
4	3	ralrimiva 2871	. . 3
5		r19.29_2a.2	. . 3
6	4, 5	r19.29d2r 3000	. 2
7		pm3.35 587	. . . . 5
8	7	ancoms 453	. . . 4
9	8	rexlimivw 2946	. . 3
10	9	rexlimivw 2946	. 2
11	6, 10	syl 16	1

Syntax hints:  ->wi 4  /\wa 369  e.wcel 1818  A.wral 2807  E.wrex 2808

This theorem is referenced by:  trust  20732  utoptop  20737  metusttoOLD  21060  metustto  21061  restmetu  21090  tgbtwndiff  23897  legov  23972  legso  23985  tglnne  24008  tglndim0  24009  tglinethru  24016  tglnne0  24020  tglnpt2  24021  footex  24095  midex  24111  opptgdim2  24117  f1otrge  24175  archiabllem2c  27739  txomap  27837  qtophaus  27839  pstmfval  27875  eulerpartlemgvv  28315  irrapxlem4  30761

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-ral 2812  df-rex 2813