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 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