MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  orcs Structured version   Visualization version   GIF version

Theorem orcs 873
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.)
Hypothesis
Ref Expression
orcs.1 ((𝜑𝜓) → 𝜒)
Assertion
Ref Expression
orcs (𝜑𝜒)

Proof of Theorem orcs
StepHypRef Expression
1 orc 865 . 2 (𝜑 → (𝜑𝜓))
2 orcs.1 . 2 ((𝜑𝜓) → 𝜒)
31, 2syl 17 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 845
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 206  df-or 846
This theorem is referenced by:  olcs  874  ifor  4538  tppreqb  4763  frxp  8054  mndifsplit  21969  maducoeval2  21973  leibpilem2  26275  leibpi  26276  3o1cs  31278  3o2cs  31279  poimirlem31  36076  tsan2  36568  frege114d  41972  ntrneiel2  42300  nnfoctbdjlem  44628
  Copyright terms: Public domain W3C validator