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 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