![]() |
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 3112. 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 1912 | . 2 ⊢ Ⅎ𝑥𝜒 | |
3 | r19.29af.1 | . 2 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒) | |
4 | r19.29af.2 | . 2 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓) | |
5 | 1, 2, 3, 4 | r19.29af2 3265 | 1 ⊢ (𝜑 → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 Ⅎwnf 1780 ∈ wcel 2106 ∃wrex 3068 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-12 2175 |
This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1777 df-nf 1781 df-ral 3060 df-rex 3069 |
This theorem is referenced by: fsnex 7303 neiptopnei 23156 neitr 23204 utopsnneiplem 24272 isucn2 24304 2sqmo 27496 foresf1o 32532 fsumiunle 32836 nsgqusf1olem3 33423 irngnzply1 33706 reff 33800 locfinreflem 33801 ordtconnlem1 33885 esumrnmpt2 34049 esumgect 34071 esum2dlem 34073 esum2d 34074 esumiun 34075 sigapildsys 34143 oms0 34279 eulerpartlemgvv 34358 breprexplema 34624 stoweidlem27 45983 stoweidlem35 45991 |
Copyright terms: Public domain | W3C validator |