![]() |
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 3114, version with two restricted quantifiers. (Contributed by Thierry Arnoux, 26-Nov-2017.) (Proof shortened by Wolf Lammen, 4-Nov-2024.) |
Ref | Expression |
---|---|
r19.29vva.1 | ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ 𝜓) → 𝜒) |
r19.29vva.2 | ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓) |
Ref | Expression |
---|---|
r19.29vva | ⊢ (𝜑 → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | r19.29vva.1 | . . 3 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ 𝜓) → 𝜒) | |
2 | r19.29vva.2 | . . 3 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓) | |
3 | 1, 2 | reximddv2 3203 | . 2 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒) |
4 | idd 24 | . . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝜒 → 𝜒)) | |
5 | 4 | rexlimivv 3193 | . 2 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒 → 𝜒) |
6 | 3, 5 | syl 17 | 1 ⊢ (𝜑 → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 ∈ wcel 2107 ∃wrex 3070 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 df-rex 3071 |
This theorem is referenced by: trust 23597 utoptop 23602 metustto 23925 restmetu 23942 tgbtwndiff 27490 legov 27569 legso 27583 tglnne 27612 tglndim0 27613 tglinethru 27620 tglnne0 27624 tglnpt2 27625 footexALT 27702 footex 27705 midex 27721 opptgdim2 27729 cgrane1 27796 cgrane2 27797 cgrane3 27798 cgrane4 27799 cgrahl1 27800 cgrahl2 27801 cgracgr 27802 cgratr 27807 cgrabtwn 27810 cgrahl 27811 dfcgra2 27814 sacgr 27815 acopyeu 27818 f1otrge 27856 suppovss 31644 cyc3genpm 32050 cyc3conja 32055 archiabllem2c 32080 ringlsmss1 32225 ringlsmss2 32226 mxidlprm 32285 lindsunlem 32376 dimkerim 32379 txomap 32472 qtophaus 32474 pstmfval 32534 eulerpartlemgvv 33033 tgoldbachgtd 33332 irrapxlem4 41191 |
Copyright terms: Public domain | W3C validator |