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 958 | 1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → (𝜒 ∨ 𝜃))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ wo 841 |
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 208 df-an 397 df-or 842 |
This theorem is referenced by: pm2.38 962 pm2.8 966 pm2.73 967 pm2.74 968 pm2.82 969 moeq3 3700 unss1 4152 ordtri2or2 6280 gchor 10037 relin01 11152 icombl 24092 ioombl 24093 coltr 26360 frgrregorufrg 28032 cycpmco2 30702 fmlasuc 32530 satffunlem1lem2 32547 satffunlem2lem2 32550 naim1 33634 onsucconni 33682 dnibndlem13 33726 mblfinlem2 34811 leat3 36311 meetat2 36313 paddss1 36833 |
Copyright terms: Public domain | W3C validator |