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

Theorem r19.29af 3254
 Description: A commonly used pattern based on r19.29 3181. See r19.29a 3213, r19.29an 3212 for a variant when 𝑥 is disjoint from 𝜑. (Contributed by Thierry Arnoux, 29-Nov-2017.)
Hypotheses
Ref Expression
r19.29af.0 𝑥𝜑
r19.29af.1 (((𝜑𝑥𝐴) ∧ 𝜓) → 𝜒)
r19.29af.2 (𝜑 → ∃𝑥𝐴 𝜓)
Assertion
Ref Expression
r19.29af (𝜑𝜒)
Distinct variable group:   𝜒,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem r19.29af
StepHypRef Expression
1 r19.29af.0 . 2 𝑥𝜑
2 nfv 1915 . 2 𝑥𝜒
3 r19.29af.1 . 2 (((𝜑𝑥𝐴) ∧ 𝜓) → 𝜒)
4 r19.29af.2 . 2 (𝜑 → ∃𝑥𝐴 𝜓)
51, 2, 3, 4r19.29af2 3253 1 (𝜑𝜒)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399  Ⅎwnf 1785   ∈ wcel 2111  ∃wrex 3071 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-12 2175 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-nf 1786  df-ral 3075  df-rex 3076 This theorem is referenced by:  fsnex  7031  neiptopnei  21832  neitr  21880  utopsnneiplem  22948  isucn2  22980  2sqmo  26120  foresf1o  30372  fsumiunle  30667  nsgqusf1olem3  31121  reff  31310  locfinreflem  31311  ordtconnlem1  31395  esumrnmpt2  31555  esumgect  31577  esum2dlem  31579  esum2d  31580  esumiun  31581  sigapildsys  31649  oms0  31783  eulerpartlemgvv  31862  breprexplema  32129  stoweidlem27  43035  stoweidlem35  43043
 Copyright terms: Public domain W3C validator