| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > 3jaodan | Structured version Visualization version GIF version | ||
| Description: Disjunction of three antecedents (deduction). (Contributed by NM, 14-Oct-2005.) |
| Ref | Expression |
|---|---|
| 3jaodan.1 | ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
| 3jaodan.2 | ⊢ ((𝜑 ∧ 𝜃) → 𝜒) |
| 3jaodan.3 | ⊢ ((𝜑 ∧ 𝜏) → 𝜒) |
| Ref | Expression |
|---|---|
| 3jaodan | ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃 ∨ 𝜏)) → 𝜒) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 3jaodan.1 | . . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | |
| 2 | 1 | ex 412 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) |
| 3 | 3jaodan.2 | . . . 4 ⊢ ((𝜑 ∧ 𝜃) → 𝜒) | |
| 4 | 3 | ex 412 | . . 3 ⊢ (𝜑 → (𝜃 → 𝜒)) |
| 5 | 3jaodan.3 | . . . 4 ⊢ ((𝜑 ∧ 𝜏) → 𝜒) | |
| 6 | 5 | ex 412 | . . 3 ⊢ (𝜑 → (𝜏 → 𝜒)) |
| 7 | 2, 4, 6 | 3jaod 1431 | . 2 ⊢ (𝜑 → ((𝜓 ∨ 𝜃 ∨ 𝜏) → 𝜒)) |
| 8 | 7 | imp 406 | 1 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃 ∨ 𝜏)) → 𝜒) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∨ w3o 1086 |
| 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 849 df-3or 1088 df-3an 1089 |
| This theorem is referenced by: mpjao3dan 1434 onzsl 7867 zeo 12704 xrltnsym 13179 xrlttri 13181 xrlttr 13182 qbtwnxr 13242 xltnegi 13258 xaddcom 13282 xnegdi 13290 xsubge0 13303 xrub 13354 bpoly3 16094 blssioo 24816 ismbf2d 25675 itg2seq 25777 eliccioo 32913 3ccased 35719 lineelsb2 36149 sticksstones1 42147 dfxlim2v 45862 usgrexmpl2trifr 47996 |
| Copyright terms: Public domain | W3C validator |