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

Theorem orcnd 878
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 871 . 2 (𝜑 → (𝜒𝜓))
3 orcnd.2 . 2 (𝜑 → ¬ 𝜓)
42, 3olcnd 877 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  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:  poxp2  8166  poxp3  8173  nnaordex2  8675  fpwwe2lem12  10679  evlslem3  22121  psdmul  22187  fzone1  32807  ccatws1f1o  32920  chnub  32985  0ringsubrg  33237  drngidl  33440  mxidlmaxv  33475  mxidlprm  33477  rprmasso2  33533  1arithidom  33544  zringidom  33558  fldext2chn  33733  aks6d1c2p2  42100  aks6d1c5  42120
  Copyright terms: Public domain W3C validator