![]() |
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 4321 nnawordex 6532 exmidontri2or 7244 addlocprlem 7536 nqprloc 7546 ltexprlemrl 7611 aptiprleml 7640 aptiprlemu 7641 elnn0z 9268 zaddcl 9295 zletric 9299 zlelttric 9300 zltnle 9301 zdceq 9330 zdcle 9331 zdclt 9332 nn01to3 9619 xposdif 9884 fzdcel 10042 qletric 10246 qlelttric 10247 qltnle 10248 qdceq 10249 frec2uzlt2d 10406 triap 14862 tridceq 14889 |
Copyright terms: Public domain | W3C validator |