![]() |
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 3201. See r19.29a 3235, r19.29an 3234 for a variant when 𝑥 is disjoint from 𝜑. (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 1873 | . 2 ⊢ Ⅎ𝑥𝜒 | |
3 | r19.29af.1 | . 2 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒) | |
4 | r19.29af.2 | . 2 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓) | |
5 | 1, 2, 3, 4 | r19.29af2 3272 | 1 ⊢ (𝜑 → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 387 Ⅎwnf 1746 ∈ wcel 2050 ∃wrex 3090 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-12 2106 |
This theorem depends on definitions: df-bi 199 df-an 388 df-ex 1743 df-nf 1747 df-ral 3094 df-rex 3095 |
This theorem is referenced by: r19.29anOLD 3274 r19.29aOLD 3275 fsnex 6864 neiptopnei 21444 neitr 21492 utopsnneiplem 22559 isucn2 22591 2sqmo 25715 foresf1o 30044 fsumiunle 30291 reff 30744 locfinreflem 30745 ordtconnlem1 30808 esumrnmpt2 30968 esumgect 30990 esum2dlem 30992 esum2d 30993 esumiun 30994 sigapildsys 31063 oms0 31197 eulerpartlemgvv 31276 breprexplema 31546 stoweidlem27 41741 stoweidlem35 41749 |
Copyright terms: Public domain | W3C validator |