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 3260
Description: A commonly used pattern based on r19.29 3251, version with two restricted quantifiers. (Contributed by Thierry Arnoux, 26-Nov-2017.)
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 . . . . . 6 ((((𝜑𝑥𝐴) ∧ 𝑦𝐵) ∧ 𝜓) → 𝜒)
21ex 402 . . . . 5 (((𝜑𝑥𝐴) ∧ 𝑦𝐵) → (𝜓𝜒))
32ralrimiva 3145 . . . 4 ((𝜑𝑥𝐴) → ∀𝑦𝐵 (𝜓𝜒))
43ralrimiva 3145 . . 3 (𝜑 → ∀𝑥𝐴𝑦𝐵 (𝜓𝜒))
5 r19.29vva.2 . . 3 (𝜑 → ∃𝑥𝐴𝑦𝐵 𝜓)
64, 5r19.29d2r 3259 . 2 (𝜑 → ∃𝑥𝐴𝑦𝐵 ((𝜓𝜒) ∧ 𝜓))
7 pm3.35 838 . . . . 5 ((𝜓 ∧ (𝜓𝜒)) → 𝜒)
87ancoms 451 . . . 4 (((𝜓𝜒) ∧ 𝜓) → 𝜒)
98rexlimivw 3208 . . 3 (∃𝑦𝐵 ((𝜓𝜒) ∧ 𝜓) → 𝜒)
109rexlimivw 3208 . 2 (∃𝑥𝐴𝑦𝐵 ((𝜓𝜒) ∧ 𝜓) → 𝜒)
116, 10syl 17 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 385  wcel 2157  wral 3087  wrex 3088
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006
This theorem depends on definitions:  df-bi 199  df-an 386  df-ex 1876  df-ral 3092  df-rex 3093
This theorem is referenced by:  trust  22358  utoptop  22363  metustto  22683  restmetu  22700  tgbtwndiff  25750  legov  25829  legso  25843  tglnne  25872  tglndim0  25873  tglinethru  25880  tglnne0  25884  tglnpt2  25885  footex  25962  midex  25978  opptgdim2  25986  cgrane1  26053  cgrane2  26054  cgrane3  26055  cgrane4  26056  cgrahl1  26057  cgrahl2  26058  cgracgr  26059  cgratr  26064  cgrabtwn  26066  cgrahl  26067  dfcgra2  26070  sacgr  26071  acopyeu  26074  f1otrge  26101  archiabllem2c  30257  txomap  30409  qtophaus  30411  pstmfval  30447  eulerpartlemgvv  30946  tgoldbachgtd  31252  irrapxlem4  38163
  Copyright terms: Public domain W3C validator