![]() |
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 867 | . 2 ⊢ (𝜑 → (𝜑 ∨ 𝜓)) | |
2 | orcs.1 | . 2 ⊢ ((𝜑 ∨ 𝜓) → 𝜒) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ wo 847 |
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 848 |
This theorem is referenced by: olcs 876 ifor 4585 tppreqb 4810 frxp 8150 mndifsplit 22658 maducoeval2 22662 leibpilem2 26999 leibpi 27000 3o1cs 32490 3o2cs 32491 elrgspnlem2 33233 poimirlem31 37638 tsan2 38129 frege114d 43748 ntrneiel2 44076 nnfoctbdjlem 46411 |
Copyright terms: Public domain | W3C validator |