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 3074
Description: A commonly used pattern based on r19.29 3066, 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 450 . . . . 5 (((𝜑𝑥𝐴) ∧ 𝑦𝐵) → (𝜓𝜒))
32ralrimiva 2961 . . . 4 ((𝜑𝑥𝐴) → ∀𝑦𝐵 (𝜓𝜒))
43ralrimiva 2961 . . 3 (𝜑 → ∀𝑥𝐴𝑦𝐵 (𝜓𝜒))
5 r19.29vva.2 . . 3 (𝜑 → ∃𝑥𝐴𝑦𝐵 𝜓)
64, 5r19.29d2r 3073 . 2 (𝜑 → ∃𝑥𝐴𝑦𝐵 ((𝜓𝜒) ∧ 𝜓))
7 pm3.35 610 . . . . 5 ((𝜓 ∧ (𝜓𝜒)) → 𝜒)
87ancoms 469 . . . 4 (((𝜓𝜒) ∧ 𝜓) → 𝜒)
98rexlimivw 3023 . . 3 (∃𝑦𝐵 ((𝜓𝜒) ∧ 𝜓) → 𝜒)
109rexlimivw 3023 . 2 (∃𝑥𝐴𝑦𝐵 ((𝜓𝜒) ∧ 𝜓) → 𝜒)
116, 10syl 17 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wcel 1987  wral 2907  wrex 2908
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702  df-ral 2912  df-rex 2913
This theorem is referenced by:  trust  21952  utoptop  21957  metustto  22277  restmetu  22294  tgbtwndiff  25314  legov  25393  legso  25407  tglnne  25436  tglndim0  25437  tglinethru  25444  tglnne0  25448  tglnpt2  25449  footex  25526  midex  25542  opptgdim2  25550  cgrane1  25617  cgrane2  25618  cgrane3  25619  cgrane4  25620  cgrahl1  25621  cgrahl2  25622  cgracgr  25623  cgratr  25628  cgrabtwn  25630  cgrahl  25631  dfcgra2  25634  sacgr  25635  acopyeu  25638  f1otrge  25665  archiabllem2c  29552  txomap  29701  qtophaus  29703  pstmfval  29739  eulerpartlemgvv  30237  irrapxlem4  36896
  Copyright terms: Public domain W3C validator