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  20660  maducoeval2  20664  leibpilem2  24889  leibpi  24890  3o1cs  29649  3o2cs  29650  poimirlem31  33773  tsan2  34281  frege114d  38576  ntrneiel2  38910  nnfoctbdjlem  41189
 Copyright terms: Public domain W3C validator