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

Theorem r19.29af 3271
Description: A commonly used pattern based on r19.29 3125. See r19.29a 3170, r19.29an 3166 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 1934 . 2 𝑥𝜒
3 r19.29af.1 . 2 (((𝜑𝑥𝐴) ∧ 𝜓) → 𝜒)
4 r19.29af.2 . 2 (𝜑 → ∃𝑥𝐴 𝜓)
51, 2, 3, 4r19.29af2 3270 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  wnf 1803  wcel 2142  wrex 3086
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-12 2212
This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-nf 1804  df-ral 3077  df-rex 3087
This theorem is referenced by:  fsnex  7267  neiptopnei  23192  neitr  23240  utopsnneiplem  24307  isucn2  24338  2sqmo  27501  foresf1o  32703  fsumiunle  33031  nsgqusf1olem3  33601  irngnzply1  33988  reff  34136  locfinreflem  34137  ordtconnlem1  34221  esumrnmpt2  34365  esumgect  34387  esum2dlem  34389  esum2d  34390  esumiun  34391  sigapildsys  34459  oms0  34594  eulerpartlemgvv  34673  breprexplema  34924  stoweidlem27  46601  stoweidlem35  46609
  Copyright terms: Public domain W3C validator