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 707 | . 2 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → 𝜒)) |
5 | 1, 4 | mpd 13 | 1 ⊢ (𝜑 → 𝜒) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∨ wo 698 |
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 699 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: ifbothdc 3547 opth1 4208 onsucelsucexmidlem 4500 reldmtpos 6212 dftpos4 6222 nnm00 6488 xpfi 6886 omp1eomlem 7050 ctmlemr 7064 ctssdclemn0 7066 finomni 7095 indpi 7274 enq0tr 7366 prarloclem3step 7428 distrlem4prl 7516 distrlem4pru 7517 lelttr 7978 nn1suc 8867 nnsub 8887 nn0lt2 9263 uzin 9489 xrlelttr 9733 xlesubadd 9810 fzfig 10355 seq3id 10433 seq3z 10436 faclbnd 10643 facavg 10648 bcval5 10665 hashfzo 10724 iserex 11266 fsum3cvg 11305 fsumf1o 11317 fisumss 11319 fsumcl2lem 11325 fsumadd 11333 fsummulc2 11375 isumsplit 11418 fprodf1o 11515 prodssdc 11516 fprodssdc 11517 fprodmul 11518 absdvdsb 11735 dvdsabsb 11736 dvdsabseq 11770 m1exp1 11823 flodddiv4 11856 gcdaddm 11902 gcdabs1 11907 lcmdvds 11990 prmind2 12031 rpexp 12064 fermltl 12145 pcxnn0cl 12221 pcxcl 12222 pcabs 12236 pcmpt 12252 pockthg 12266 trilpolemcl 13757 trilpolemlt1 13761 |
Copyright terms: Public domain | W3C validator |