![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > r19.29vva | Structured version Visualization version GIF version |
Description: A commonly used pattern based on r19.29 3101, version with two restricted quantifiers. (Contributed by Thierry Arnoux, 26-Nov-2017.) |
Ref | Expression |
---|---|
r19.29vva.1 | ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ 𝜓) → 𝜒) |
r19.29vva.2 | ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓) |
Ref | Expression |
---|---|
r19.29vva | ⊢ (𝜑 → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | r19.29vva.1 | . . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ 𝜓) → 𝜒) | |
2 | 1 | ex 449 | . . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝜓 → 𝜒)) |
3 | 2 | ralrimiva 2995 | . . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ 𝐵 (𝜓 → 𝜒)) |
4 | 3 | ralrimiva 2995 | . . 3 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜓 → 𝜒)) |
5 | r19.29vva.2 | . . 3 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓) | |
6 | 4, 5 | r19.29d2r 3109 | . 2 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ((𝜓 → 𝜒) ∧ 𝜓)) |
7 | pm3.35 610 | . . . . 5 ⊢ ((𝜓 ∧ (𝜓 → 𝜒)) → 𝜒) | |
8 | 7 | ancoms 468 | . . . 4 ⊢ (((𝜓 → 𝜒) ∧ 𝜓) → 𝜒) |
9 | 8 | rexlimivw 3058 | . . 3 ⊢ (∃𝑦 ∈ 𝐵 ((𝜓 → 𝜒) ∧ 𝜓) → 𝜒) |
10 | 9 | rexlimivw 3058 | . 2 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ((𝜓 → 𝜒) ∧ 𝜓) → 𝜒) |
11 | 6, 10 | syl 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 |