![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mpjao3dan | GIF version |
Description: Eliminate a 3-way disjunction in a deduction. (Contributed by Thierry Arnoux, 13-Apr-2018.) |
Ref | Expression |
---|---|
mpjao3dan.1 | ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
mpjao3dan.2 | ⊢ ((𝜑 ∧ 𝜃) → 𝜒) |
mpjao3dan.3 | ⊢ ((𝜑 ∧ 𝜏) → 𝜒) |
mpjao3dan.4 | ⊢ (𝜑 → (𝜓 ∨ 𝜃 ∨ 𝜏)) |
Ref | Expression |
---|---|
mpjao3dan | ⊢ (𝜑 → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpjao3dan.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | |
2 | mpjao3dan.2 | . . 3 ⊢ ((𝜑 ∧ 𝜃) → 𝜒) | |
3 | 1, 2 | jaodan 797 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃)) → 𝜒) |
4 | mpjao3dan.3 | . 2 ⊢ ((𝜑 ∧ 𝜏) → 𝜒) | |
5 | mpjao3dan.4 | . . 3 ⊢ (𝜑 → (𝜓 ∨ 𝜃 ∨ 𝜏)) | |
6 | df-3or 979 | . . 3 ⊢ ((𝜓 ∨ 𝜃 ∨ 𝜏) ↔ ((𝜓 ∨ 𝜃) ∨ 𝜏)) | |
7 | 5, 6 | sylib 122 | . 2 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ∨ 𝜏)) |
8 | 3, 4, 7 | mpjaodan 798 | 1 ⊢ (𝜑 → 𝜒) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ∨ wo 708 ∨ 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 |
This theorem is referenced by: wetriext 4575 nntri3 6495 nntri2or2 6496 nntr2 6501 tridc 6896 nnnninfeq 7123 exmidontriimlem2 7218 caucvgprlemnkj 7662 caucvgprlemnbj 7663 caucvgprprlemnkj 7688 caucvgprprlemnbj 7689 caucvgsr 7798 npnflt 9811 nmnfgt 9814 xleadd1a 9869 xltadd1 9872 xlt2add 9876 xsubge0 9877 xleaddadd 9883 addmodlteq 10393 iseqf1olemkle 10479 hashfiv01gt1 10755 xrmaxltsup 11259 xrmaxadd 11262 xrbdtri 11277 cvgratz 11533 zdvdsdc 11812 divalglemeunn 11918 divalglemex 11919 divalglemeuneg 11920 divalg 11921 znege1 12170 ennnfonelemk 12393 isxmet2d 13719 trilpolemres 14650 trirec0 14652 |
Copyright terms: Public domain | W3C validator |