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 3264
Description: A commonly used pattern based on r19.29 3113. See r19.29a 3161, r19.29an 3157 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 1916 . 2 𝑥𝜒
3 r19.29af.1 . 2 (((𝜑𝑥𝐴) ∧ 𝜓) → 𝜒)
4 r19.29af.2 . 2 (𝜑 → ∃𝑥𝐴 𝜓)
51, 2, 3, 4r19.29af2 3263 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wnf 1784  wcel 2105  wrex 3069
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-12 2170
This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-nf 1785  df-ral 3061  df-rex 3070
This theorem is referenced by:  fsnex  7284  neiptopnei  22956  neitr  23004  utopsnneiplem  24072  isucn2  24104  2sqmo  27283  foresf1o  32175  fsumiunle  32468  nsgqusf1olem3  32966  irngnzply1  33210  reff  33283  locfinreflem  33284  ordtconnlem1  33368  esumrnmpt2  33530  esumgect  33552  esum2dlem  33554  esum2d  33555  esumiun  33556  sigapildsys  33624  oms0  33760  eulerpartlemgvv  33839  breprexplema  34106  stoweidlem27  45202  stoweidlem35  45210
  Copyright terms: Public domain W3C validator