![]() |
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 1916 | . 2 ⊢ Ⅎ𝑥𝜒 | |
3 | r19.29af.1 | . 2 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒) | |
4 | r19.29af.2 | . 2 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓) | |
5 | 1, 2, 3, 4 | r19.29af2 3263 | 1 ⊢ (𝜑 → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 Ⅎwnf 1784 ∈ wcel 2105 ∃wrex 3069 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-12 2170 |
This theorem depends on definitions: df-bi 206 df-an 396 df-ex 1781 df-nf 1785 df-ral 3061 df-rex 3070 |
This theorem is referenced by: fsnex 7284 neiptopnei 22956 neitr 23004 utopsnneiplem 24072 isucn2 24104 2sqmo 27283 foresf1o 32175 fsumiunle 32468 nsgqusf1olem3 32966 irngnzply1 33210 reff 33283 locfinreflem 33284 ordtconnlem1 33368 esumrnmpt2 33530 esumgect 33552 esum2dlem 33554 esum2d 33555 esumiun 33556 sigapildsys 33624 oms0 33760 eulerpartlemgvv 33839 breprexplema 34106 stoweidlem27 45202 stoweidlem35 45210 |
Copyright terms: Public domain | W3C validator |