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 1279 | . 2 ⊢ (((𝜓 → 𝜒) ∧ (𝜃 → 𝜒) ∧ (𝜏 → 𝜒)) → ((𝜓 ∨ 𝜃 ∨ 𝜏) → 𝜒)) | |
5 | 1, 2, 3, 4 | syl3anc 1216 | 1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃 ∨ 𝜏) → 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∨ w3o 961 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 698 |
This theorem depends on definitions: df-bi 116 df-3or 963 df-3an 964 |
This theorem is referenced by: 3jaodan 1284 3jaao 1286 issod 4241 nnawordex 6424 addlocprlem 7343 nqprloc 7353 ltexprlemrl 7418 aptiprleml 7447 aptiprlemu 7448 elnn0z 9067 zaddcl 9094 zletric 9098 zlelttric 9099 zltnle 9100 zdceq 9126 zdcle 9127 zdclt 9128 nn01to3 9409 xposdif 9665 fzdcel 9820 qletric 10021 qlelttric 10022 qltnle 10023 qdceq 10024 frec2uzlt2d 10177 triap 13224 |
Copyright terms: Public domain | W3C validator |