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 3110
Description: A commonly used pattern based on r19.29 3101, 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 2995 . . . 4 ((𝜑𝑥𝐴) → ∀𝑦𝐵 (𝜓𝜒))
43ralrimiva 2995 . . 3 (𝜑 → ∀𝑥𝐴𝑦𝐵 (𝜓𝜒))
5 r19.29vva.2 . . 3 (𝜑 → ∃𝑥𝐴𝑦𝐵 𝜓)
64, 5r19.29d2r 3109 . 2 (𝜑 → ∃𝑥𝐴𝑦𝐵 ((𝜓𝜒) ∧ 𝜓))
7 pm3.35 610 . . . . 5 ((𝜓 ∧ (𝜓𝜒)) → 𝜒)
87ancoms 468 . . . 4 (((𝜓𝜒) ∧ 𝜓) → 𝜒)
98rexlimivw 3058 . . 3 (∃𝑦𝐵 ((𝜓𝜒) ∧ 𝜓) → 𝜒)
109rexlimivw 3058 . 2 (∃𝑥𝐴𝑦𝐵 ((𝜓𝜒) ∧ 𝜓) → 𝜒)
116, 10syl 17 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wcel 2030  wral 2941  wrex 2942
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-ral 2946  df-rex 2947
This theorem is referenced by:  trust  22080  utoptop  22085  metustto  22405  restmetu  22422  tgbtwndiff  25446  legov  25525  legso  25539  tglnne  25568  tglndim0  25569  tglinethru  25576  tglnne0  25580  tglnpt2  25581  footex  25658  midex  25674  opptgdim2  25682  cgrane1  25749  cgrane2  25750  cgrane3  25751  cgrane4  25752  cgrahl1  25753  cgrahl2  25754  cgracgr  25755  cgratr  25760  cgrabtwn  25762  cgrahl  25763  dfcgra2  25766  sacgr  25767  acopyeu  25770  f1otrge  25797  archiabllem2c  29877  txomap  30029  qtophaus  30031  pstmfval  30067  eulerpartlemgvv  30566  tgoldbachgtd  30868  irrapxlem4  37706
  Copyright terms: Public domain W3C validator