| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > orim1d | Structured version Visualization version GIF version | ||
| Description: Disjoin antecedents and consequents in a deduction. (Contributed by NM, 23-Apr-1995.) |
| Ref | Expression |
|---|---|
| orim1d.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
| Ref | Expression |
|---|---|
| orim1d | ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → (𝜒 ∨ 𝜃))) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | orim1d.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
| 2 | idd 24 | . 2 ⊢ (𝜑 → (𝜃 → 𝜃)) | |
| 3 | 1, 2 | orim12d 967 | 1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → (𝜒 ∨ 𝜃))) |
| Colors of variables: wff setvar class |
| Syntax hints: → 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-an 396 df-or 849 |
| This theorem is referenced by: pm2.38 971 pm2.8 975 pm2.73 976 pm2.74 977 pm2.82 978 moeq3 3718 unss1 4185 ordtri2or2 6483 gchor 10667 relin01 11787 icombl 25599 ioombl 25600 coltr 28655 frgrregorufrg 30345 cycpmco2 33153 fmlasuc 35391 satffunlem1lem2 35408 satffunlem2lem2 35411 naim1 36390 onsucconni 36438 dnibndlem13 36491 mblfinlem2 37665 leat3 39296 meetat2 39298 paddss1 39819 onov0suclim 43287 dflim5 43342 ordsssucim 43415 |
| Copyright terms: Public domain | W3C validator |