Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > orim2d | 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 |
---|---|
orim2d | ⊢ (𝜑 → ((𝜃 ∨ 𝜓) → (𝜃 ∨ 𝜒))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | idd 24 | . 2 ⊢ (𝜑 → (𝜃 → 𝜃)) | |
2 | orim1d.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
3 | 1, 2 | orim12d 883 | 1 ⊢ (𝜑 → ((𝜃 ∨ 𝜓) → (𝜃 ∨ 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ wo 383 |
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 197 df-or 385 df-an 386 |
This theorem is referenced by: orim2 886 pm2.82 897 poxp 7289 soxp 7290 relin01 10552 nneo 11461 uzp1 11721 vdwlem9 15693 dfconn2 21222 fin1aufil 21736 dgrlt 24022 aalioulem2 24088 aalioulem5 24091 aalioulem6 24092 aaliou 24093 sqff1o 24908 disjpreima 29397 disjdsct 29480 voliune 30292 volfiniune 30293 naim2 32385 paddss2 35104 lzunuz 37331 acongneg2 37544 nneom 42321 |
Copyright terms: Public domain | W3C validator |