![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3jaod | GIF version |
Description: Disjunction of 3 antecedents (deduction). (Contributed by NM, 14-Oct-2005.) |
Ref | Expression |
---|---|
3jaod.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
3jaod.2 | ⊢ (𝜑 → (𝜃 → 𝜒)) |
3jaod.3 | ⊢ (𝜑 → (𝜏 → 𝜒)) |
Ref | Expression |
---|---|
3jaod | ⊢ (𝜑 → ((𝜓 ∨ 𝜃 ∨ 𝜏) → 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3jaod.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
2 | 3jaod.2 | . 2 ⊢ (𝜑 → (𝜃 → 𝜒)) | |
3 | 3jaod.3 | . 2 ⊢ (𝜑 → (𝜏 → 𝜒)) | |
4 | 3jao 1301 | . 2 ⊢ (((𝜓 → 𝜒) ∧ (𝜃 → 𝜒) ∧ (𝜏 → 𝜒)) → ((𝜓 ∨ 𝜃 ∨ 𝜏) → 𝜒)) | |
5 | 1, 2, 3, 4 | syl3anc 1238 | 1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃 ∨ 𝜏) → 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∨ w3o 977 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 709 |
This theorem depends on definitions: df-bi 117 df-3or 979 df-3an 980 |
This theorem is referenced by: 3jaodan 1306 3jaao 1308 issod 4319 nnawordex 6529 exmidontri2or 7241 addlocprlem 7533 nqprloc 7543 ltexprlemrl 7608 aptiprleml 7637 aptiprlemu 7638 elnn0z 9265 zaddcl 9292 zletric 9296 zlelttric 9297 zltnle 9298 zdceq 9327 zdcle 9328 zdclt 9329 nn01to3 9616 xposdif 9881 fzdcel 10039 qletric 10243 qlelttric 10244 qltnle 10245 qdceq 10246 frec2uzlt2d 10403 triap 14713 tridceq 14740 |
Copyright terms: Public domain | W3C validator |