Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > orri | Structured version Visualization version GIF version |
Description: Infer disjunction from implication. (Contributed by NM, 11-Jun-1994.) |
Ref | Expression |
---|---|
orri.1 | ⊢ (¬ 𝜑 → 𝜓) |
Ref | Expression |
---|---|
orri | ⊢ (𝜑 ∨ 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | orri.1 | . 2 ⊢ (¬ 𝜑 → 𝜓) | |
2 | df-or 844 | . 2 ⊢ ((𝜑 ∨ 𝜓) ↔ (¬ 𝜑 → 𝜓)) | |
3 | 1, 2 | mpbir 233 | 1 ⊢ (𝜑 ∨ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∨ wo 843 |
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 209 df-or 844 |
This theorem is referenced by: orci 861 olci 862 pm2.25 886 curryax 890 exmid 891 pm2.13 894 pm5.11g 940 pm5.12 942 pm5.14 943 pm5.55 945 pm3.12 990 pm5.15 1009 pm5.54 1014 4exmid 1046 rb-ax2 1750 rb-ax3 1751 rb-ax4 1752 exmo 2620 axi12 2789 axi12OLD 2790 axbndOLD 2792 exmidne 3026 ifeqor 4516 fvbr0 6692 letrii 10759 clwwlknondisj 27884 poimirlem26 34912 tsbi3 35407 tsan2 35414 tsan3 35415 clsk1indlem2 40385 |
Copyright terms: Public domain | W3C validator |