Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ex | Structured version Visualization version GIF version |
Description: Exportation inference. (This theorem used to be labeled "exp" but was changed to "ex" so as not to conflict with the math token "exp", per the June 2006 Metamath spec change.) A translation of natural deduction rule → I (→ introduction), see natded 28110. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Eric Schmidt, 22-Dec-2006.) |
Ref | Expression |
---|---|
ex.1 | ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
Ref | Expression |
---|---|
ex | ⊢ (𝜑 → (𝜓 → 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-an 397 | . . 3 ⊢ ((𝜑 ∧ 𝜓) ↔ ¬ (𝜑 → ¬ 𝜓)) | |
2 | ex.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | |
3 | 1, 2 | sylbir 236 | . 2 ⊢ (¬ (𝜑 → ¬ 𝜓) → 𝜒) |
4 | 3 | expi 166 | 1 ⊢ (𝜑 → (𝜓 → 𝜒)) |
Copyright terms: Public domain | W3C validator |