| 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 872 | . 2 ⊢ (𝜑 → (𝜒 ∨ 𝜓)) |
| 3 | orcnd.2 | . 2 ⊢ (𝜑 → ¬ 𝜓) | |
| 4 | 2, 3 | olcnd 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 |