Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ori | Structured version Visualization version GIF version |
Description: Infer implication from disjunction. (Contributed by NM, 11-Jun-1994.) |
Ref | Expression |
---|---|
ori.1 | ⊢ (𝜑 ∨ 𝜓) |
Ref | Expression |
---|---|
ori | ⊢ (¬ 𝜑 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ori.1 | . 2 ⊢ (𝜑 ∨ 𝜓) | |
2 | df-or 384 | . 2 ⊢ ((𝜑 ∨ 𝜓) ↔ (¬ 𝜑 → 𝜓)) | |
3 | 1, 2 | mpbi 219 | 1 ⊢ (¬ 𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∨ wo 382 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 196 df-or 384 |
This theorem is referenced by: 3ori 1380 mtpor 1686 exmoeu 2490 moanim 2517 moexex 2529 mo2icl 3352 mosubopt 4897 fvrn0 6126 eliman0 6133 dff3 6280 onuninsuci 6932 omelon2 6969 infensuc 8023 rankxpsuc 8628 cardlim 8681 alephreg 9283 tskcard 9482 sinhalfpilem 24019 sltres 31061 |
Copyright terms: Public domain | W3C validator |