|   | 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 3113. See r19.29a 3161, r19.29an 3157 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 1913 | . 2 ⊢ Ⅎ𝑥𝜒 | |
| 3 | r19.29af.1 | . 2 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒) | |
| 4 | r19.29af.2 | . 2 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓) | |
| 5 | 1, 2, 3, 4 | r19.29af2 3266 | 1 ⊢ (𝜑 → 𝜒) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∧ wa 395 Ⅎwnf 1782 ∈ wcel 2107 ∃wrex 3069 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-12 2176 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1779 df-nf 1783 df-ral 3061 df-rex 3070 | 
| This theorem is referenced by: fsnex 7304 neiptopnei 23141 neitr 23189 utopsnneiplem 24257 isucn2 24289 2sqmo 27482 foresf1o 32524 fsumiunle 32832 nsgqusf1olem3 33444 irngnzply1 33742 reff 33839 locfinreflem 33840 ordtconnlem1 33924 esumrnmpt2 34070 esumgect 34092 esum2dlem 34094 esum2d 34095 esumiun 34096 sigapildsys 34164 oms0 34300 eulerpartlemgvv 34379 breprexplema 34646 stoweidlem27 46047 stoweidlem35 46055 | 
| Copyright terms: Public domain | W3C validator |