![]() |
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 718 | . 2 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → 𝜒)) |
5 | 1, 4 | mpd 13 | 1 ⊢ (𝜑 → 𝜒) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∨ wo 709 |
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 710 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: ifbothdc 3582 opth1 4254 onsucelsucexmidlem 4546 reldmtpos 6279 dftpos4 6289 nnm00 6556 xpfi 6959 omp1eomlem 7124 ctmlemr 7138 ctssdclemn0 7140 finomni 7169 indpi 7372 enq0tr 7464 prarloclem3step 7526 distrlem4prl 7614 distrlem4pru 7615 lelttr 8077 nn1suc 8969 nnsub 8989 nn0lt2 9365 uzin 9592 xrlelttr 9838 xlesubadd 9915 fzfig 10463 seq3id 10541 seq3z 10544 faclbnd 10756 facavg 10761 bcval5 10778 hashfzo 10837 iserex 11382 fsum3cvg 11421 fsumf1o 11433 fisumss 11435 fsumcl2lem 11441 fsumadd 11449 fsummulc2 11491 isumsplit 11534 fprodf1o 11631 prodssdc 11632 fprodssdc 11633 fprodmul 11634 absdvdsb 11851 dvdsabsb 11852 dvdsabseq 11888 m1exp1 11941 flodddiv4 11974 gcdaddm 12020 gcdabs1 12025 lcmdvds 12114 prmind2 12155 rpexp 12188 fermltl 12269 pcxnn0cl 12345 pcxcl 12346 pcabs 12361 pcmpt 12378 pockthg 12392 mulgnn0ass 13115 lgseisenlem2 14929 trilpolemcl 15264 trilpolemlt1 15268 |
Copyright terms: Public domain | W3C validator |