![]() |
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 3212 | . 2 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒) |
4 | idd 24 | . . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝜒 → 𝜒)) | |
5 | 4 | rexlimivv 3199 | . 2 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒 → 𝜒) |
6 | 3, 5 | syl 17 | 1 ⊢ (𝜑 → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∈ wcel 2106 ∃wrex 3070 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1782 df-rex 3071 |
This theorem is referenced by: trust 23741 utoptop 23746 metustto 24069 restmetu 24086 tgbtwndiff 27795 legov 27874 legso 27888 tglnne 27917 tglndim0 27918 tglinethru 27925 tglnne0 27929 tglnpt2 27930 footexALT 28007 footex 28010 midex 28026 opptgdim2 28034 cgrane1 28101 cgrane2 28102 cgrane3 28103 cgrane4 28104 cgrahl1 28105 cgrahl2 28106 cgracgr 28107 cgratr 28112 cgrabtwn 28115 cgrahl 28116 dfcgra2 28119 sacgr 28120 acopyeu 28123 f1otrge 28161 suppovss 31944 cyc3genpm 32352 cyc3conja 32357 archiabllem2c 32382 ringlsmss1 32551 ringlsmss2 32552 mxidlprm 32631 qsdrngilem 32653 lindsunlem 32768 dimkerim 32771 txomap 32883 qtophaus 32885 pstmfval 32945 eulerpartlemgvv 33444 tgoldbachgtd 33743 irrapxlem4 41645 |
Copyright terms: Public domain | W3C validator |