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

Theorem r19.29vva 3334
 Description: A commonly used pattern based on r19.29 3252, version with two restricted quantifiers. (Contributed by Thierry Arnoux, 26-Nov-2017.) (Proof shortened by Wolf Lammen, 29-Jun-2023.)
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 3276 . 2 (𝜑 → ∃𝑥𝐴𝑦𝐵 𝜒)
4 id 22 . . . 4 (𝜒𝜒)
54rexlimivw 3280 . . 3 (∃𝑦𝐵 𝜒𝜒)
65reximi 3241 . 2 (∃𝑥𝐴𝑦𝐵 𝜒 → ∃𝑥𝐴 𝜒)
74rexlimivw 3280 . 2 (∃𝑥𝐴 𝜒𝜒)
83, 6, 73syl 18 1 (𝜑𝜒)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2107  ∃wrex 3137 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904 This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1774  df-ral 3141  df-rex 3142 This theorem is referenced by:  trust  22830  utoptop  22835  metustto  23155  restmetu  23172  tgbtwndiff  26284  legov  26363  legso  26377  tglnne  26406  tglndim0  26407  tglinethru  26414  tglnne0  26418  tglnpt2  26419  footexALT  26496  footex  26499  midex  26515  opptgdim2  26523  cgrane1  26590  cgrane2  26591  cgrane3  26592  cgrane4  26593  cgrahl1  26594  cgrahl2  26595  cgracgr  26596  cgratr  26601  cgrabtwn  26604  cgrahl  26605  dfcgra2  26608  sacgr  26609  acopyeu  26612  f1otrge  26650  suppovss  30418  cyc3genpm  30787  cyc3conja  30792  archiabllem2c  30817  mxidlprm  30969  lindsunlem  31008  dimkerim  31011  txomap  31086  qtophaus  31088  pstmfval  31124  eulerpartlemgvv  31622  tgoldbachgtd  31921  irrapxlem4  39407
 Copyright terms: Public domain W3C validator