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 965 | 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 210 df-an 400 df-or 848 |
This theorem is referenced by: orim2 968 pm2.82 976 poxp 7895 soxp 7896 relin01 11356 nneo 12261 uzp1 12475 vdwlem9 16542 dfconn2 22316 fin1aufil 22829 dgrlt 25160 aalioulem2 25226 aalioulem5 25229 aalioulem6 25230 aaliou 25231 sqff1o 26064 disjpreima 30642 disjdsct 30755 voliune 31909 volfiniune 31910 satfvsucsuc 33040 naim2 34316 paddss2 37569 lzunuz 40293 acongneg2 40502 nneom 45546 |
Copyright terms: Public domain | W3C validator |