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

Theorem orcs 875
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 867 . 2 (𝜑 → (𝜑𝜓))
2 orcs.1 . 2 ((𝜑𝜓) → 𝜒)
31, 2syl 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 210  df-or 848
This theorem is referenced by:  olcs  876  ifor  4493  tppreqb  4718  frxp  7893  mndifsplit  21533  maducoeval2  21537  leibpilem2  25824  leibpi  25825  3o1cs  30531  3o2cs  30532  poimirlem31  35545  tsan2  36037  frege114d  41043  ntrneiel2  41373  nnfoctbdjlem  43668
  Copyright terms: Public domain W3C validator