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 792 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃)) → 𝜒) |
4 | mpjao3dan.3 | . 2 ⊢ ((𝜑 ∧ 𝜏) → 𝜒) | |
5 | mpjao3dan.4 | . . 3 ⊢ (𝜑 → (𝜓 ∨ 𝜃 ∨ 𝜏)) | |
6 | df-3or 974 | . . 3 ⊢ ((𝜓 ∨ 𝜃 ∨ 𝜏) ↔ ((𝜓 ∨ 𝜃) ∨ 𝜏)) | |
7 | 5, 6 | sylib 121 | . 2 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ∨ 𝜏)) |
8 | 3, 4, 7 | mpjaodan 793 | 1 ⊢ (𝜑 → 𝜒) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∨ wo 703 ∨ w3o 972 |
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 704 |
This theorem depends on definitions: df-bi 116 df-3or 974 |
This theorem is referenced by: wetriext 4561 nntri3 6476 nntri2or2 6477 nntr2 6482 tridc 6877 nnnninfeq 7104 exmidontriimlem2 7199 caucvgprlemnkj 7628 caucvgprlemnbj 7629 caucvgprprlemnkj 7654 caucvgprprlemnbj 7655 caucvgsr 7764 npnflt 9772 nmnfgt 9775 xleadd1a 9830 xltadd1 9833 xlt2add 9837 xsubge0 9838 xleaddadd 9844 addmodlteq 10354 iseqf1olemkle 10440 hashfiv01gt1 10716 xrmaxltsup 11221 xrmaxadd 11224 xrbdtri 11239 cvgratz 11495 zdvdsdc 11774 divalglemeunn 11880 divalglemex 11881 divalglemeuneg 11882 divalg 11883 znege1 12132 ennnfonelemk 12355 isxmet2d 13142 trilpolemres 14074 trirec0 14076 |
Copyright terms: Public domain | W3C validator |