![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > r19.29af | Structured version Visualization version GIF version |
Description: A commonly used pattern based on r19.29 3101. (Contributed by Thierry Arnoux, 29-Nov-2017.) |
Ref | Expression |
---|---|
r19.29af.0 | ⊢ Ⅎ𝑥𝜑 |
r19.29af.1 | ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒) |
r19.29af.2 | ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓) |
Ref | Expression |
---|---|
r19.29af | ⊢ (𝜑 → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | r19.29af.0 | . 2 ⊢ Ⅎ𝑥𝜑 | |
2 | nfv 1883 | . 2 ⊢ Ⅎ𝑥𝜒 | |
3 | r19.29af.1 | . 2 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒) | |
4 | r19.29af.2 | . 2 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓) | |
5 | 1, 2, 3, 4 | r19.29af2 3104 | 1 ⊢ (𝜑 → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 Ⅎwnf 1748 ∈ wcel 2030 ∃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 ax-6 1945 ax-7 1981 ax-12 2087 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-ex 1745 df-nf 1750 df-ral 2946 df-rex 2947 |
This theorem is referenced by: r19.29an 3106 r19.29a 3107 elsnxpOLD 5716 fsnex 6578 neiptopnei 20984 neitr 21032 utopsnneiplem 22098 isucn2 22130 foresf1o 29469 fsumiunle 29703 2sqmo 29777 reff 30034 locfinreflem 30035 ordtconnlem1 30098 esumrnmpt2 30258 esumgect 30280 esum2dlem 30282 esum2d 30283 esumiun 30284 sigapildsys 30353 oms0 30487 eulerpartlemgvv 30566 breprexplema 30836 stoweidlem27 40562 stoweidlem35 40570 |
Copyright terms: Public domain | W3C validator |