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

Theorem r19.29af 3058
 Description: A commonly used pattern based on r19.29 3054. (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 1830 . 2 𝑥𝜒
3 r19.29af.1 . 2 (((𝜑𝑥𝐴) ∧ 𝜓) → 𝜒)
4 r19.29af.2 . 2 (𝜑 → ∃𝑥𝐴 𝜓)
51, 2, 3, 4r19.29af2 3057 1 (𝜑𝜒)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383  Ⅎwnf 1699   ∈ wcel 1977  ∃wrex 2897 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-ex 1696  df-nf 1701  df-ral 2901  df-rex 2902 This theorem is referenced by:  r19.29an  3059  r19.29a  3060  elsnxpOLD  5595  fsnex  6438  neiptopnei  20746  neitr  20794  utopsnneiplem  21861  isucn2  21893  foresf1o  28727  2sqmo  28980  reff  29234  locfinreflem  29235  ordtconlem1  29298  esumrnmpt2  29457  esumgect  29479  esum2dlem  29481  esum2d  29482  esumiun  29483  sigapildsys  29552  oms0  29686  eulerpartlemgvv  29765  stoweidlem27  38920  stoweidlem35  38928
 Copyright terms: Public domain W3C validator