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

Theorem r19.29an 3106
 Description: A commonly used pattern based on r19.29 3101. (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 1883 . . 3 𝑥𝜑
2 nfre1 3034 . . 3 𝑥𝑥𝐴 𝜓
31, 2nfan 1868 . 2 𝑥(𝜑 ∧ ∃𝑥𝐴 𝜓)
4 r19.29an.1 . . 3 (((𝜑𝑥𝐴) ∧ 𝜓) → 𝜒)
54adantllr 755 . 2 ((((𝜑 ∧ ∃𝑥𝐴 𝜓) ∧ 𝑥𝐴) ∧ 𝜓) → 𝜒)
6 simpr 476 . 2 ((𝜑 ∧ ∃𝑥𝐴 𝜓) → ∃𝑥𝐴 𝜓)
73, 5, 6r19.29af 3105 1 ((𝜑 ∧ ∃𝑥𝐴 𝜓) → 𝜒)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∈ wcel 2030  ∃wrex 2942 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-10 2059  ax-12 2087 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-ral 2946  df-rex 2947 This theorem is referenced by:  summolem2  14491  cygabl  18338  dissnlocfin  21380  utopsnneiplem  22098  restmetu  22422  elqaa  24122  colline  25589  f1otrg  25796  axcontlem2  25890  grpoidinvlem4  27489  2sqmo  29777  isarchi3  29869  fimaproj  30028  qtophaus  30031  locfinreflem  30035  cmpcref  30045  ordtconnlem1  30098  esumpcvgval  30268  esumcvg  30276  eulerpartlems  30550  eulerpartlemgvv  30566  reprinfz1  30828  reprpmtf1o  30832  isbnd3  33713  eldiophss  37655  eldioph4b  37692  pellfund14b  37780  opeoALTV  41920
 Copyright terms: Public domain W3C validator