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

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
StepHypRef Expression
1 nfv 1707 . . 3
2 nfre1 2918 . . 3
31, 2nfan 1928 . 2
4 r19.29an.1 . . 3
54adantllr 718 . 2
6 simpr 461 . 2
73, 5, 6r19.29af 2997 1
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator