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 3216
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 3215 . 2 (𝜑 → ∃𝑥𝐴𝑦𝐵 𝜒)
4 idd 24 . . 3 ((𝑥𝐴𝑦𝐵) → (𝜒𝜒))
54rexlimivv 3201 . 2 (∃𝑥𝐴𝑦𝐵 𝜒𝜒)
63, 5syl 17 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wcel 2108  wrex 3070
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3071
This theorem is referenced by:  trust  24238  utoptop  24243  metustto  24566  restmetu  24583  tgbtwndiff  28514  legov  28593  legso  28607  tglnne  28636  tglndim0  28637  tglinethru  28644  tglnne0  28648  tglnpt2  28649  footexALT  28726  footex  28729  midex  28745  opptgdim2  28753  cgrane1  28820  cgrane2  28821  cgrane3  28822  cgrane4  28823  cgrahl1  28824  cgrahl2  28825  cgracgr  28826  cgratr  28831  cgrabtwn  28834  cgrahl  28835  dfcgra2  28838  sacgr  28839  acopyeu  28842  f1otrge  28880  suppovss  32690  cyc3genpm  33172  cyc3conja  33177  archiabllem2c  33202  elrgspnsubrunlem2  33252  rloccring  33274  rloc1r  33276  fracfld  33310  ringlsmss1  33424  ringlsmss2  33425  mxidlprm  33498  qsdrngilem  33522  zringfrac  33582  lindsunlem  33675  dimkerim  33678  txomap  33833  qtophaus  33835  pstmfval  33895  eulerpartlemgvv  34378  tgoldbachgtd  34677  primrootscoprmpow  42100  posbezout  42101  primrootscoprbij2  42104  primrootspoweq0  42107  aks6d1c2lem4  42128  aks6d1c2  42131  aks6d1c6lem3  42173  aks6d1c6lem5  42178  irrapxlem4  42836
  Copyright terms: Public domain W3C validator