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

Theorem r19.29an 3225
Description: A commonly used pattern based on r19.29 3220. (Contributed by Thierry Arnoux, 29-Dec-2019.)
Hypothesis
Ref Expression
r19.29an.1 (((𝜑𝑥𝐴) ∧ 𝜓) → 𝜒)
Assertion
Ref Expression
r19.29an ((𝜑 ∧ ∃𝑥𝐴 𝜓) → 𝜒)
Distinct variable groups:   𝜒,𝑥   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem r19.29an
StepHypRef Expression
1 nfv 1995 . . 3 𝑥𝜑
2 nfre1 3153 . . 3 𝑥𝑥𝐴 𝜓
31, 2nfan 1980 . 2 𝑥(𝜑 ∧ ∃𝑥𝐴 𝜓)
4 r19.29an.1 . . 3 (((𝜑𝑥𝐴) ∧ 𝜓) → 𝜒)
54adantllr 698 . 2 ((((𝜑 ∧ ∃𝑥𝐴 𝜓) ∧ 𝑥𝐴) ∧ 𝜓) → 𝜒)
6 simpr 471 . 2 ((𝜑 ∧ ∃𝑥𝐴 𝜓) → ∃𝑥𝐴 𝜓)
73, 5, 6r19.29af 3224 1 ((𝜑 ∧ ∃𝑥𝐴 𝜓) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wcel 2145  wrex 3062
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-10 2174  ax-12 2203
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-ral 3066  df-rex 3067
This theorem is referenced by:  summolem2  14655  cygabl  18499  dissnlocfin  21553  utopsnneiplem  22271  restmetu  22595  elqaa  24297  colline  25765  f1otrg  25972  axcontlem2  26066  grpoidinvlem4  27701  2sqmo  29989  isarchi3  30081  fimaproj  30240  qtophaus  30243  locfinreflem  30247  cmpcref  30257  ordtconnlem1  30310  esumpcvgval  30480  esumcvg  30488  eulerpartlems  30762  eulerpartlemgvv  30778  reprinfz1  31040  reprpmtf1o  31044  isbnd3  33913  eldiophss  37862  eldioph4b  37899  pellfund14b  37987  opeoALTV  42118
  Copyright terms: Public domain W3C validator