Theorem r19.29an 2998

Description: A commonly used pattern based on r19.29 2992. (Contributed by Thierry Arnoux, 29-Dec-2019.)

Hypothesis

Ref	Expression
r19.29an.1

Assertion

Ref	Expression
r19.29an

Distinct variable groups:   ,   ,

Proof of Theorem r19.29an

Step	Hyp	Ref	Expression
1		nfv 1707	. . 3
2		nfre1 2918	. . 3
3	1, 2	nfan 1928	. 2
4		r19.29an.1	. . 3
5	4	adantllr 718	. 2
6		simpr 461	. 2
7	3, 5, 6	r19.29af 2997	1

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

This theorem is referenced by:  summolem2  13538  cygabl  16893  dissnlocfin  20030  utopsnneiplem  20750  restmetu  21090  elqaa  22718  colline  24030  f1otrg  24174  axcontlem2  24268  grpoidinvlem4  25209  2sqmo  27637  isarchi3  27731  fimaproj  27836  qtophaus  27839  locfinreflem  27843  cmpcref  27853  ordtconlem1  27906  esumpcvgval  28084  esumcvg  28092  eulerpartlems  28299  eulerpartlemgvv  28315  isbnd3  30280  eldiophss  30708  eldioph4b  30745  pellfund14b  30835

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  ax-6 1747  ax-7 1790  ax-10 1837  ax-12 1854

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