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

Theorem orcnd 879
Description: A lemma for Conjunctive Normal Form unit propagation, in deduction form. (Contributed by Giovanni Mascellani, 15-Sep-2017.)
Hypotheses
Ref Expression
orcnd.1 (𝜑 → (𝜓𝜒))
orcnd.2 (𝜑 → ¬ 𝜓)
Assertion
Ref Expression
orcnd (𝜑𝜒)

Proof of Theorem orcnd
StepHypRef Expression
1 orcnd.1 . . 3 (𝜑 → (𝜓𝜒))
21orcomd 872 . 2 (𝜑 → (𝜒𝜓))
3 orcnd.2 . 2 (𝜑 → ¬ 𝜓)
42, 3olcnd 878 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  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:  poxp2  8168  poxp3  8175  nnaordex2  8677  fpwwe2lem12  10682  evlslem3  22104  psdmul  22170  fzone1  32802  ccatws1f1o  32936  chnub  33002  0ringsubrg  33255  drngidl  33461  mxidlmaxv  33496  mxidlprm  33498  rprmasso2  33554  1arithidom  33565  zringidom  33579  fldext2chn  33769  aks6d1c2p2  42120  aks6d1c5  42140
  Copyright terms: Public domain W3C validator