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 3072, 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 450 | . . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝜓 → 𝜒)) |
3 | 2 | ralrimiva 2966 | . . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ 𝐵 (𝜓 → 𝜒)) |
4 | 3 | ralrimiva 2966 | . . 3 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜓 → 𝜒)) |
5 | r19.29vva.2 | . . 3 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓) | |
6 | 4, 5 | r19.29d2r 3080 | . 2 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ((𝜓 → 𝜒) ∧ 𝜓)) |
7 | pm3.35 611 | . . . . 5 ⊢ ((𝜓 ∧ (𝜓 → 𝜒)) → 𝜒) | |
8 | 7 | ancoms 469 | . . . 4 ⊢ (((𝜓 → 𝜒) ∧ 𝜓) → 𝜒) |
9 | 8 | rexlimivw 3029 | . . 3 ⊢ (∃𝑦 ∈ 𝐵 ((𝜓 → 𝜒) ∧ 𝜓) → 𝜒) |
10 | 9 | rexlimivw 3029 | . 2 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ((𝜓 → 𝜒) ∧ 𝜓) → 𝜒) |
11 | 6, 10 | syl 17 | 1 ⊢ (𝜑 → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 384 ∈ wcel 1990 ∀wral 2912 ∃wrex 2913 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 |
This theorem depends on definitions: df-bi 197 df-an 386 df-ex 1705 df-ral 2917 df-rex 2918 |
This theorem is referenced by: trust 22033 utoptop 22038 metustto 22358 restmetu 22375 tgbtwndiff 25401 legov 25480 legso 25494 tglnne 25523 tglndim0 25524 tglinethru 25531 tglnne0 25535 tglnpt2 25536 footex 25613 midex 25629 opptgdim2 25637 cgrane1 25704 cgrane2 25705 cgrane3 25706 cgrane4 25707 cgrahl1 25708 cgrahl2 25709 cgracgr 25710 cgratr 25715 cgrabtwn 25717 cgrahl 25718 dfcgra2 25721 sacgr 25722 acopyeu 25725 f1otrge 25752 archiabllem2c 29749 txomap 29901 qtophaus 29903 pstmfval 29939 eulerpartlemgvv 30438 tgoldbachgtd 30740 irrapxlem4 37389 |
Copyright terms: Public domain | W3C validator |