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 3333
Description: A commonly used pattern based on r19.29 3251, 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 3275 . 2 (𝜑 → ∃𝑥𝐴𝑦𝐵 𝜒)
4 id 22 . . . 4 (𝜒𝜒)
54rexlimivw 3279 . . 3 (∃𝑦𝐵 𝜒𝜒)
65reximi 3240 . 2 (∃𝑥𝐴𝑦𝐵 𝜒 → ∃𝑥𝐴 𝜒)
74rexlimivw 3279 . 2 (∃𝑥𝐴 𝜒𝜒)
83, 6, 73syl 18 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wcel 2105  wrex 3136
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-ral 3140  df-rex 3141
This theorem is referenced by:  trust  22765  utoptop  22770  metustto  23090  restmetu  23107  tgbtwndiff  26219  legov  26298  legso  26312  tglnne  26341  tglndim0  26342  tglinethru  26349  tglnne0  26353  tglnpt2  26354  footexALT  26431  footex  26434  midex  26450  opptgdim2  26458  cgrane1  26525  cgrane2  26526  cgrane3  26527  cgrane4  26528  cgrahl1  26529  cgrahl2  26530  cgracgr  26531  cgratr  26536  cgrabtwn  26539  cgrahl  26540  dfcgra2  26543  sacgr  26544  acopyeu  26547  f1otrge  26585  suppovss  30354  cyc3genpm  30721  cyc3conja  30726  archiabllem2c  30751  lindsunlem  30919  dimkerim  30922  txomap  30997  qtophaus  30999  pstmfval  31035  eulerpartlemgvv  31533  tgoldbachgtd  31832  irrapxlem4  39300
  Copyright terms: Public domain W3C validator