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

Theorem orcs 876
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 868 . 2 (𝜑 → (𝜑𝜓))
2 orcs.1 . 2 ((𝜑𝜓) → 𝜒)
31, 2syl 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