![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > ori | Unicode 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 370 | . 2 | |
3 | 1, 2 | mpbi 208 | 1 |
Colors of variables: wff setvar class |
Syntax hints: -. wn 3 -> wi 4
\/ wo 368 |
This theorem is referenced by: 3ori 1288 mtpor 1603 exmoeu 2316 moanim 2350 moexex 2363 mo2icl 3278 mosubopt 4750 fvrn0 5893 eliman0 5900 dff3 6044 onuninsuci 6675 omelon2 6712 infensuc 7715 rankxpsuc 8321 cardlim 8374 alephreg 8978 tskcard 9180 sinhalfpilem 22856 sltres 29424 |
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 185 df-or 370 |
Copyright terms: Public domain | W3C validator |