![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > orcnd | Structured version Visualization version GIF version |
Description: A lemma for Conjunctive Normal Form unit propagation, in deduction form. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
Ref | Expression |
---|---|
orcnd.1 | ⊢ (𝜑 → (𝜓 ∨ 𝜒)) |
orcnd.2 | ⊢ (𝜑 → ¬ 𝜓) |
Ref | Expression |
---|---|
orcnd | ⊢ (𝜑 → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | orcnd.1 | . . 3 ⊢ (𝜑 → (𝜓 ∨ 𝜒)) | |
2 | 1 | orcomd 871 | . 2 ⊢ (𝜑 → (𝜒 ∨ 𝜓)) |
3 | orcnd.2 | . 2 ⊢ (𝜑 → ¬ 𝜓) | |
4 | 2, 3 | olcnd 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 |