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 3254
Description: A commonly used pattern based on r19.29 3118. See r19.29a 3160, r19.29an 3156 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 1918 . 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 397  wnf 1786  wcel 2107  wrex 3074
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-12 2172
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-nf 1787  df-ral 3066  df-rex 3075
This theorem is referenced by:  fsnex  7234  neiptopnei  22499  neitr  22547  utopsnneiplem  23615  isucn2  23647  2sqmo  26801  foresf1o  31473  fsumiunle  31767  nsgqusf1olem3  32233  irngnzply1  32405  reff  32460  locfinreflem  32461  ordtconnlem1  32545  esumrnmpt2  32707  esumgect  32729  esum2dlem  32731  esum2d  32732  esumiun  32733  sigapildsys  32801  oms0  32937  eulerpartlemgvv  33016  breprexplema  33283  stoweidlem27  44342  stoweidlem35  44350
  Copyright terms: Public domain W3C validator