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 3054, 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 2949 | . . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ 𝐵 (𝜓 → 𝜒)) |
4 | 3 | ralrimiva 2949 | . . 3 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜓 → 𝜒)) |
5 | r19.29vva.2 | . . 3 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓) | |
6 | 4, 5 | r19.29d2r 3061 | . 2 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ((𝜓 → 𝜒) ∧ 𝜓)) |
7 | pm3.35 609 | . . . . 5 ⊢ ((𝜓 ∧ (𝜓 → 𝜒)) → 𝜒) | |
8 | 7 | ancoms 468 | . . . 4 ⊢ (((𝜓 → 𝜒) ∧ 𝜓) → 𝜒) |
9 | 8 | rexlimivw 3011 | . . 3 ⊢ (∃𝑦 ∈ 𝐵 ((𝜓 → 𝜒) ∧ 𝜓) → 𝜒) |
10 | 9 | rexlimivw 3011 | . 2 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ((𝜓 → 𝜒) ∧ 𝜓) → 𝜒) |
11 | 6, 10 | syl 17 | 1 ⊢ (𝜑 → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∈ wcel 1977 ∀wral 2896 ∃wrex 2897 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 |
This theorem depends on definitions: df-bi 196 df-an 385 df-ex 1696 df-ral 2901 df-rex 2902 |
This theorem is referenced by: trust 21843 utoptop 21848 metustto 22168 restmetu 22185 tgbtwndiff 25201 legov 25280 legso 25294 tglnne 25323 tglndim0 25324 tglinethru 25331 tglnne0 25335 tglnpt2 25336 footex 25413 midex 25429 opptgdim2 25437 cgrane1 25504 cgrane2 25505 cgrane3 25506 cgrane4 25507 cgrahl1 25508 cgrahl2 25509 cgracgr 25510 cgratr 25515 cgrabtwn 25517 cgrahl 25518 dfcgra2 25521 sacgr 25522 acopyeu 25525 f1otrge 25552 archiabllem2c 29080 txomap 29229 qtophaus 29231 pstmfval 29267 eulerpartlemgvv 29765 irrapxlem4 36407 |
Copyright terms: Public domain | W3C validator |