| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > nfim | Structured version Visualization version GIF version | ||
| Description: If 𝑥 is not free in 𝜑 and 𝜓, then it is not free in (𝜑 → 𝜓). Inference associated with nfimt 1895. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.) df-nf 1784 changed. (Revised by Wolf Lammen, 17-Sep-2021.) |
| Ref | Expression |
|---|---|
| nfim.1 | ⊢ Ⅎ𝑥𝜑 |
| nfim.2 | ⊢ Ⅎ𝑥𝜓 |
| Ref | Expression |
|---|---|
| nfim | ⊢ Ⅎ𝑥(𝜑 → 𝜓) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nfim.1 | . 2 ⊢ Ⅎ𝑥𝜑 | |
| 2 | nfim.2 | . 2 ⊢ Ⅎ𝑥𝜓 | |
| 3 | nfimt 1895 | . 2 ⊢ ((Ⅎ𝑥𝜑 ∧ Ⅎ𝑥𝜓) → Ⅎ𝑥(𝜑 → 𝜓)) | |
| 4 | 1, 2, 3 | mp2an 692 | 1 ⊢ Ⅎ𝑥(𝜑 → 𝜓) |
| Copyright terms: Public domain | W3C validator |