![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mpjaod | Structured version Visualization version 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 394 | . 2 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → 𝜒)) |
5 | 1, 4 | mpd 15 | 1 ⊢ (𝜑 → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ wo 382 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 197 df-or 384 |
This theorem is referenced by: ecase2d 1000 opth1 4973 sorpssun 6986 sorpssin 6987 reldmtpos 7405 dftpos4 7416 oaass 7686 nnawordex 7762 omabs 7772 suplub2 8408 en3lplem2 8550 cantnflt 8607 cantnfp1lem3 8615 tcrank 8785 cardaleph 8950 fpwwe2 9503 gchpwdom 9530 grur1 9680 indpi 9767 nn1suc 11079 nnsub 11097 seqid 12886 seqz 12889 faclbnd 13117 facavg 13128 bcval5 13145 hashnnn0genn0 13171 hashfzo 13254 sqrlem6 14032 resqrex 14035 absmod0 14087 absz 14095 iserex 14431 fsumf1o 14498 fsumss 14500 fsumcl2lem 14506 fsumadd 14514 fsummulc2 14560 fsumconst 14566 fsumrelem 14583 isumsplit 14616 fprodf1o 14720 fprodss 14722 fprodcl2lem 14724 fprodmul 14734 fproddiv 14735 fprodconst 14752 fprodn0 14753 absdvdsb 15047 dvdsabsb 15048 gcdabs1 15298 bezoutlem1 15303 bezoutlem2 15304 isprm5 15466 pcabs 15626 pockthg 15657 prmreclem5 15671 vdwlem13 15744 0ram 15771 ram0 15773 prmlem0 15859 mulgnn0ass 17625 psgnunilem2 17961 mndodcongi 18008 oddvdsnn0 18009 odnncl 18010 efgredlemb 18205 gsumzres 18356 gsumzcl2 18357 gsumzf1o 18359 gsumzaddlem 18367 gsumconst 18380 gsumzmhm 18383 gsummulglem 18387 gsumzoppg 18390 pgpfac1lem5 18524 mplsubrglem 19487 gsumfsum 19861 zringlpirlem1 19880 ordthaus 21236 icccmplem2 22673 metdstri 22701 ioombl 23379 itgabs 23646 dvlip 23801 dvge0 23814 dvivthlem1 23816 dvcnvrelem1 23825 ply1rem 23968 dgrcolem2 24075 quotcan 24109 sinq12ge0 24305 argregt0 24401 argrege0 24402 scvxcvx 24757 bpos1lem 25052 bposlem3 25056 lgseisenlem2 25146 frgrregord013 27382 htthlem 27902 atcvati 29373 sinccvglem 31692 noextendseq 31945 noetalem3 31990 midofsegid 32336 outsideofeq 32362 hfun 32410 ordcmp 32571 icoreclin 33335 itgabsnc 33609 dvasin 33626 cvrat 35026 4atlem10 35210 4atlem12 35216 cdleme18d 35900 cdleme22b 35946 cdleme32e 36050 lclkrlem2e 37117 pell1234qrdich 37742 clsk1indlem3 38658 suctrALT 39375 wallispilem3 40602 bgoldbtbnd 42022 |
Copyright terms: Public domain | W3C validator |