![]() |
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 966 | 1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → (𝜒 ∨ 𝜃))) |
Colors of variables: wff setvar class |
Syntax hints: → 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-an 396 df-or 848 |
This theorem is referenced by: pm2.38 970 pm2.8 974 pm2.73 975 pm2.74 976 pm2.82 977 moeq3 3720 unss1 4194 ordtri2or2 6484 gchor 10664 relin01 11784 icombl 25612 ioombl 25613 coltr 28669 frgrregorufrg 30354 cycpmco2 33135 fmlasuc 35370 satffunlem1lem2 35387 satffunlem2lem2 35390 naim1 36371 onsucconni 36419 dnibndlem13 36472 mblfinlem2 37644 leat3 39276 meetat2 39278 paddss1 39799 onov0suclim 43263 dflim5 43318 ordsssucim 43391 |
Copyright terms: Public domain | W3C validator |