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 415 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) |
3 | 3jaodan.2 | . . . 4 ⊢ ((𝜑 ∧ 𝜃) → 𝜒) | |
4 | 3 | ex 415 | . . 3 ⊢ (𝜑 → (𝜃 → 𝜒)) |
5 | 3jaodan.3 | . . . 4 ⊢ ((𝜑 ∧ 𝜏) → 𝜒) | |
6 | 5 | ex 415 | . . 3 ⊢ (𝜑 → (𝜏 → 𝜒)) |
7 | 2, 4, 6 | 3jaod 1423 | . 2 ⊢ (𝜑 → ((𝜓 ∨ 𝜃 ∨ 𝜏) → 𝜒)) |
8 | 7 | imp 409 | 1 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃 ∨ 𝜏)) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 ∨ w3o 1081 |
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 209 df-an 399 df-or 844 df-3or 1083 df-3an 1084 |
This theorem is referenced by: mpjao3dan 1426 onzsl 7554 zeo 12062 xrltnsym 12524 xrlttri 12526 xrlttr 12527 qbtwnxr 12587 xltnegi 12603 xaddcom 12627 xnegdi 12635 xsubge0 12648 xrub 12699 bpoly3 15407 blssioo 23398 ismbf2d 24236 itg2seq 24338 eliccioo 30607 3ccased 32970 lineelsb2 33630 dfxlim2v 42202 |
Copyright terms: Public domain | W3C validator |