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

Theorem r19.29vva 3204
Description: A commonly used pattern based on r19.29 3114, version with two restricted quantifiers. (Contributed by Thierry Arnoux, 26-Nov-2017.) (Proof shortened by Wolf Lammen, 4-Nov-2024.)
Hypotheses
Ref Expression
r19.29vva.1 ((((𝜑𝑥𝐴) ∧ 𝑦𝐵) ∧ 𝜓) → 𝜒)
r19.29vva.2 (𝜑 → ∃𝑥𝐴𝑦𝐵 𝜓)
Assertion
Ref Expression
r19.29vva (𝜑𝜒)
Distinct variable groups:   𝑦,𝐴   𝑥,𝑦,𝜒   𝜑,𝑥,𝑦
Allowed substitution hints:   𝜓(𝑥,𝑦)   𝐴(𝑥)   𝐵(𝑥,𝑦)

Proof of Theorem r19.29vva
StepHypRef Expression
1 r19.29vva.1 . . 3 ((((𝜑𝑥𝐴) ∧ 𝑦𝐵) ∧ 𝜓) → 𝜒)
2 r19.29vva.2 . . 3 (𝜑 → ∃𝑥𝐴𝑦𝐵 𝜓)
31, 2reximddv2 3203 . 2 (𝜑 → ∃𝑥𝐴𝑦𝐵 𝜒)
4 idd 24 . . 3 ((𝑥𝐴𝑦𝐵) → (𝜒𝜒))
54rexlimivv 3193 . 2 (∃𝑥𝐴𝑦𝐵 𝜒𝜒)
63, 5syl 17 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  wcel 2107  wrex 3070
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
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-rex 3071
This theorem is referenced by:  trust  23597  utoptop  23602  metustto  23925  restmetu  23942  tgbtwndiff  27490  legov  27569  legso  27583  tglnne  27612  tglndim0  27613  tglinethru  27620  tglnne0  27624  tglnpt2  27625  footexALT  27702  footex  27705  midex  27721  opptgdim2  27729  cgrane1  27796  cgrane2  27797  cgrane3  27798  cgrane4  27799  cgrahl1  27800  cgrahl2  27801  cgracgr  27802  cgratr  27807  cgrabtwn  27810  cgrahl  27811  dfcgra2  27814  sacgr  27815  acopyeu  27818  f1otrge  27856  suppovss  31644  cyc3genpm  32050  cyc3conja  32055  archiabllem2c  32080  ringlsmss1  32225  ringlsmss2  32226  mxidlprm  32285  lindsunlem  32376  dimkerim  32379  txomap  32472  qtophaus  32474  pstmfval  32534  eulerpartlemgvv  33033  tgoldbachgtd  33332  irrapxlem4  41191
  Copyright terms: Public domain W3C validator