| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > orcs | Structured version Visualization version GIF version | ||
| Description: Deduction eliminating disjunct. Notational convention: We sometimes suffix with "s" the label of an inference that manipulates an antecedent, leaving the consequent unchanged. The "s" means that the inference eliminates the need for a syllogism (syl 17) -type inference in a proof. (Contributed by NM, 21-Jun-1994.) |
| Ref | Expression |
|---|---|
| orcs.1 | ⊢ ((𝜑 ∨ 𝜓) → 𝜒) |
| Ref | Expression |
|---|---|
| orcs | ⊢ (𝜑 → 𝜒) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | orc 868 | . 2 ⊢ (𝜑 → (𝜑 ∨ 𝜓)) | |
| 2 | orcs.1 | . 2 ⊢ ((𝜑 ∨ 𝜓) → 𝜒) | |
| 3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → 𝜒) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∨ wo 848 |
| 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 207 df-or 849 |
| This theorem is referenced by: olcs 877 ifor 4580 tppreqb 4805 frxp 8151 mndifsplit 22642 maducoeval2 22646 leibpilem2 26984 leibpi 26985 3o1cs 32480 3o2cs 32481 elrgspnlem2 33247 poimirlem31 37658 tsan2 38149 frege114d 43771 ntrneiel2 44099 nnfoctbdjlem 46470 |
| Copyright terms: Public domain | W3C validator |