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 3273
Description: A commonly used pattern based on r19.29 3201. See r19.29a 3235, r19.29an 3234 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 1873 . 2 𝑥𝜒
3 r19.29af.1 . 2 (((𝜑𝑥𝐴) ∧ 𝜓) → 𝜒)
4 r19.29af.2 . 2 (𝜑 → ∃𝑥𝐴 𝜓)
51, 2, 3, 4r19.29af2 3272 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 387  wnf 1746  wcel 2050  wrex 3090
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-12 2106
This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-nf 1747  df-ral 3094  df-rex 3095
This theorem is referenced by:  r19.29anOLD  3274  r19.29aOLD  3275  fsnex  6864  neiptopnei  21444  neitr  21492  utopsnneiplem  22559  isucn2  22591  2sqmo  25715  foresf1o  30044  fsumiunle  30291  reff  30744  locfinreflem  30745  ordtconnlem1  30808  esumrnmpt2  30968  esumgect  30990  esum2dlem  30992  esum2d  30993  esumiun  30994  sigapildsys  31063  oms0  31197  eulerpartlemgvv  31276  breprexplema  31546  stoweidlem27  41741  stoweidlem35  41749
  Copyright terms: Public domain W3C validator