![]() |
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 963 | 1 ⊢ (𝜑 → ((𝜃 ∨ 𝜓) → (𝜃 ∨ 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ wo 845 |
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 206 df-an 397 df-or 846 |
This theorem is referenced by: orim2 966 pm2.82 974 poxp 8059 soxp 8060 relin01 11678 nneo 12586 uzp1 12803 vdwlem9 16860 dfconn2 22768 fin1aufil 23281 dgrlt 25625 aalioulem2 25691 aalioulem5 25694 aalioulem6 25695 aaliou 25696 sqff1o 26529 disjpreima 31500 disjdsct 31612 voliune 32819 volfiniune 32820 satfvsucsuc 33950 naim2 34853 paddss2 38272 lzunuz 41069 acongneg2 41279 nneom 46585 |
Copyright terms: Public domain | W3C validator |