Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  r19.29vva Structured version   Visualization version   GIF version

Theorem r19.29vva 3062
 Description: A commonly used pattern based on r19.29 3054, 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 449 . . . . 5 (((𝜑𝑥𝐴) ∧ 𝑦𝐵) → (𝜓𝜒))
32ralrimiva 2949 . . . 4 ((𝜑𝑥𝐴) → ∀𝑦𝐵 (𝜓𝜒))
43ralrimiva 2949 . . 3 (𝜑 → ∀𝑥𝐴𝑦𝐵 (𝜓𝜒))
5 r19.29vva.2 . . 3 (𝜑 → ∃𝑥𝐴𝑦𝐵 𝜓)
64, 5r19.29d2r 3061 . 2 (𝜑 → ∃𝑥𝐴𝑦𝐵 ((𝜓𝜒) ∧ 𝜓))
7 pm3.35 609 . . . . 5 ((𝜓 ∧ (𝜓𝜒)) → 𝜒)
87ancoms 468 . . . 4 (((𝜓𝜒) ∧ 𝜓) → 𝜒)
98rexlimivw 3011 . . 3 (∃𝑦𝐵 ((𝜓𝜒) ∧ 𝜓) → 𝜒)
109rexlimivw 3011 . 2 (∃𝑥𝐴𝑦𝐵 ((𝜓𝜒) ∧ 𝜓) → 𝜒)
116, 10syl 17 1 (𝜑𝜒)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∈ wcel 1977  ∀wral 2896  ∃wrex 2897 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827 This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-ral 2901  df-rex 2902 This theorem is referenced by:  trust  21843  utoptop  21848  metustto  22168  restmetu  22185  tgbtwndiff  25201  legov  25280  legso  25294  tglnne  25323  tglndim0  25324  tglinethru  25331  tglnne0  25335  tglnpt2  25336  footex  25413  midex  25429  opptgdim2  25437  cgrane1  25504  cgrane2  25505  cgrane3  25506  cgrane4  25507  cgrahl1  25508  cgrahl2  25509  cgracgr  25510  cgratr  25515  cgrabtwn  25517  cgrahl  25518  dfcgra2  25521  sacgr  25522  acopyeu  25525  f1otrge  25552  archiabllem2c  29080  txomap  29229  qtophaus  29231  pstmfval  29267  eulerpartlemgvv  29765  irrapxlem4  36407
 Copyright terms: Public domain W3C validator