![]() |
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 3118. See r19.29a 3160, r19.29an 3156 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 1918 | . 2 ⊢ Ⅎ𝑥𝜒 | |
3 | r19.29af.1 | . 2 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒) | |
4 | r19.29af.2 | . 2 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓) | |
5 | 1, 2, 3, 4 | r19.29af2 3253 | 1 ⊢ (𝜑 → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 Ⅎwnf 1786 ∈ wcel 2107 ∃wrex 3074 |
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 ax-6 1972 ax-7 2012 ax-12 2172 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 df-nf 1787 df-ral 3066 df-rex 3075 |
This theorem is referenced by: fsnex 7234 neiptopnei 22499 neitr 22547 utopsnneiplem 23615 isucn2 23647 2sqmo 26801 foresf1o 31473 fsumiunle 31767 nsgqusf1olem3 32233 irngnzply1 32405 reff 32460 locfinreflem 32461 ordtconnlem1 32545 esumrnmpt2 32707 esumgect 32729 esum2dlem 32731 esum2d 32732 esumiun 32733 sigapildsys 32801 oms0 32937 eulerpartlemgvv 33016 breprexplema 33283 stoweidlem27 44342 stoweidlem35 44350 |
Copyright terms: Public domain | W3C validator |