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

Theorem r19.29an 3059
 Description: A commonly used pattern based on r19.29 3054. (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 1830 . . 3 𝑥𝜑
2 nfre1 2988 . . 3 𝑥𝑥𝐴 𝜓
31, 2nfan 1816 . 2 𝑥(𝜑 ∧ ∃𝑥𝐴 𝜓)
4 r19.29an.1 . . 3 (((𝜑𝑥𝐴) ∧ 𝜓) → 𝜒)
54adantllr 751 . 2 ((((𝜑 ∧ ∃𝑥𝐴 𝜓) ∧ 𝑥𝐴) ∧ 𝜓) → 𝜒)
6 simpr 476 . 2 ((𝜑 ∧ ∃𝑥𝐴 𝜓) → ∃𝑥𝐴 𝜓)
73, 5, 6r19.29af 3058 1 ((𝜑 ∧ ∃𝑥𝐴 𝜓) → 𝜒)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∈ wcel 1977  ∃wrex 2897 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-12 2034 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-ral 2901  df-rex 2902 This theorem is referenced by:  summolem2  14294  cygabl  18115  dissnlocfin  21142  utopsnneiplem  21861  restmetu  22185  elqaa  23881  colline  25344  f1otrg  25551  axcontlem2  25645  grpoidinvlem4  26745  2sqmo  28980  isarchi3  29072  fimaproj  29228  qtophaus  29231  locfinreflem  29235  cmpcref  29245  ordtconlem1  29298  esumpcvgval  29467  esumcvg  29475  eulerpartlems  29749  eulerpartlemgvv  29765  isbnd3  32753  eldiophss  36356  eldioph4b  36393  pellfund14b  36481  opeoALTV  40133
 Copyright terms: Public domain W3C validator