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

Theorem orcs 864
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 856 . 2 (𝜑 → (𝜑𝜓))
2 orcs.1 . 2 ((𝜑𝜓) → 𝜒)
31, 2syl 17 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 836
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 197  df-or 837
This theorem is referenced by:  olcs  865  ifor  4274  tppreqb  4471  frxp  7438  mndifsplit  20656  maducoeval2  20660  leibpilem2  24885  leibpi  24886  3o1cs  29645  3o2cs  29646  poimirlem31  33769  tsan2  34277  frege114d  38573  ntrneiel2  38907  nnfoctbdjlem  41186
  Copyright terms: Public domain W3C validator