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 3229
Description: A commonly used pattern based on r19.29 3220, 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 397 . . . . 5 (((𝜑𝑥𝐴) ∧ 𝑦𝐵) → (𝜓𝜒))
32ralrimiva 3115 . . . 4 ((𝜑𝑥𝐴) → ∀𝑦𝐵 (𝜓𝜒))
43ralrimiva 3115 . . 3 (𝜑 → ∀𝑥𝐴𝑦𝐵 (𝜓𝜒))
5 r19.29vva.2 . . 3 (𝜑 → ∃𝑥𝐴𝑦𝐵 𝜓)
64, 5r19.29d2r 3228 . 2 (𝜑 → ∃𝑥𝐴𝑦𝐵 ((𝜓𝜒) ∧ 𝜓))
7 pm3.35 804 . . . . 5 ((𝜓 ∧ (𝜓𝜒)) → 𝜒)
87ancoms 455 . . . 4 (((𝜓𝜒) ∧ 𝜓) → 𝜒)
98rexlimivw 3177 . . 3 (∃𝑦𝐵 ((𝜓𝜒) ∧ 𝜓) → 𝜒)
109rexlimivw 3177 . 2 (∃𝑥𝐴𝑦𝐵 ((𝜓𝜒) ∧ 𝜓) → 𝜒)
116, 10syl 17 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wcel 2145  wral 3061  wrex 3062
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991
This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1853  df-ral 3066  df-rex 3067
This theorem is referenced by:  trust  22253  utoptop  22258  metustto  22578  restmetu  22595  tgbtwndiff  25622  legov  25701  legso  25715  tglnne  25744  tglndim0  25745  tglinethru  25752  tglnne0  25756  tglnpt2  25757  footex  25834  midex  25850  opptgdim2  25858  cgrane1  25925  cgrane2  25926  cgrane3  25927  cgrane4  25928  cgrahl1  25929  cgrahl2  25930  cgracgr  25931  cgratr  25936  cgrabtwn  25938  cgrahl  25939  dfcgra2  25942  sacgr  25943  acopyeu  25946  f1otrge  25973  archiabllem2c  30089  txomap  30241  qtophaus  30243  pstmfval  30279  eulerpartlemgvv  30778  tgoldbachgtd  31080  irrapxlem4  37915
  Copyright terms: Public domain W3C validator