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 3213
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 3212 . 2 (𝜑 → ∃𝑥𝐴𝑦𝐵 𝜒)
4 idd 24 . . 3 ((𝑥𝐴𝑦𝐵) → (𝜒𝜒))
54rexlimivv 3199 . 2 (∃𝑥𝐴𝑦𝐵 𝜒𝜒)
63, 5syl 17 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wcel 2106  wrex 3070
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-rex 3071
This theorem is referenced by:  trust  23741  utoptop  23746  metustto  24069  restmetu  24086  tgbtwndiff  27795  legov  27874  legso  27888  tglnne  27917  tglndim0  27918  tglinethru  27925  tglnne0  27929  tglnpt2  27930  footexALT  28007  footex  28010  midex  28026  opptgdim2  28034  cgrane1  28101  cgrane2  28102  cgrane3  28103  cgrane4  28104  cgrahl1  28105  cgrahl2  28106  cgracgr  28107  cgratr  28112  cgrabtwn  28115  cgrahl  28116  dfcgra2  28119  sacgr  28120  acopyeu  28123  f1otrge  28161  suppovss  31944  cyc3genpm  32352  cyc3conja  32357  archiabllem2c  32382  ringlsmss1  32551  ringlsmss2  32552  mxidlprm  32631  qsdrngilem  32653  lindsunlem  32768  dimkerim  32771  txomap  32883  qtophaus  32885  pstmfval  32945  eulerpartlemgvv  33444  tgoldbachgtd  33743  irrapxlem4  41645
  Copyright terms: Public domain W3C validator