![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mpjaod | GIF version |
Description: Eliminate a disjunction in a deduction. (Contributed by Mario Carneiro, 29-May-2016.) |
Ref | Expression |
---|---|
jaod.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
jaod.2 | ⊢ (𝜑 → (𝜃 → 𝜒)) |
jaod.3 | ⊢ (𝜑 → (𝜓 ∨ 𝜃)) |
Ref | Expression |
---|---|
mpjaod | ⊢ (𝜑 → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | jaod.3 | . 2 ⊢ (𝜑 → (𝜓 ∨ 𝜃)) | |
2 | jaod.1 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
3 | jaod.2 | . . 3 ⊢ (𝜑 → (𝜃 → 𝜒)) | |
4 | 2, 3 | jaod 717 | . 2 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → 𝜒)) |
5 | 1, 4 | mpd 13 | 1 ⊢ (𝜑 → 𝜒) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∨ wo 708 |
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 |
This theorem is referenced by: ifbothdc 3566 opth1 4232 onsucelsucexmidlem 4524 reldmtpos 6247 dftpos4 6257 nnm00 6524 xpfi 6922 omp1eomlem 7086 ctmlemr 7100 ctssdclemn0 7102 finomni 7131 indpi 7319 enq0tr 7411 prarloclem3step 7473 distrlem4prl 7561 distrlem4pru 7562 lelttr 8023 nn1suc 8914 nnsub 8934 nn0lt2 9310 uzin 9536 xrlelttr 9780 xlesubadd 9857 fzfig 10403 seq3id 10481 seq3z 10484 faclbnd 10692 facavg 10697 bcval5 10714 hashfzo 10773 iserex 11318 fsum3cvg 11357 fsumf1o 11369 fisumss 11371 fsumcl2lem 11377 fsumadd 11385 fsummulc2 11427 isumsplit 11470 fprodf1o 11567 prodssdc 11568 fprodssdc 11569 fprodmul 11570 absdvdsb 11787 dvdsabsb 11788 dvdsabseq 11823 m1exp1 11876 flodddiv4 11909 gcdaddm 11955 gcdabs1 11960 lcmdvds 12049 prmind2 12090 rpexp 12123 fermltl 12204 pcxnn0cl 12280 pcxcl 12281 pcabs 12295 pcmpt 12311 pockthg 12325 mulgnn0ass 12894 trilpolemcl 14408 trilpolemlt1 14412 |
Copyright terms: Public domain | W3C validator |