![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mpjaod | Structured version Visualization version Unicode 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 382 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | mpd 15 |
1
![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() |
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 189 df-or 372 |
This theorem is referenced by: ecase2d 952 opth1 4678 sorpssun 6583 sorpssin 6584 reldmtpos 6986 dftpos4 6997 oaass 7267 nnawordex 7343 omabs 7353 suplub2 7980 en3lplem2 8125 cantnflt 8182 cantnfp1lem3 8190 tcrank 8360 cardaleph 8525 fpwwe2 9073 gchpwdom 9100 grur1 9250 indpi 9337 nn1suc 10637 nnsub 10655 seqid 12265 seqz 12268 faclbnd 12482 facavg 12493 bcval5 12510 hashnnn0genn0 12533 hashfzo 12608 sqrlem6 13323 resqrex 13326 absmod0 13378 absz 13386 iserex 13732 fsumf1o 13801 fsumss 13803 fsumcl2lem 13809 fsumadd 13817 fsummulc2 13857 fsumconst 13863 fsumrelem 13879 isumsplit 13910 fprodf1o 14012 fprodss 14014 fprodcl2lem 14016 fprodmul 14026 fproddiv 14027 fprodconst 14044 fprodn0 14045 absdvdsb 14333 dvdsabsb 14334 gcdabs1 14510 bezoutlem1 14515 bezoutlem2OLD 14516 bezoutlem2 14519 isprm5 14663 pcabs 14836 pockthg 14862 prmreclem5 14876 vdwlem13 14955 0ram 14990 ram0 14992 prmlem0 15089 mulgnn0ass 16799 psgnunilem2 17148 mndodcongi 17204 oddvdsnn0 17205 odnncl 17206 efgredlemb 17408 gsumzres 17555 gsumzcl2 17556 gsumzf1o 17558 gsumzaddlem 17566 gsumconst 17579 gsumzmhm 17582 gsummulglem 17586 gsumzoppg 17589 pgpfac1lem5 17724 mplsubrglem 18675 gsumfsum 19046 zringlpirlem1 19065 ordthaus 20412 icccmplem2 21853 metdstri 21880 metdstriOLD 21895 ioombl 22530 itgabs 22804 dvlip 22957 dvge0 22970 dvivthlem1 22972 dvcnvrelem1 22981 ply1rem 23126 dgrcolem2 23240 quotcan 23274 sinq12ge0 23475 argregt0 23571 argrege0 23572 scvxcvx 23923 bpos1lem 24222 bposlem3 24226 lgseisenlem2 24290 frgraregord013 25858 gxneg 26006 gxsuc 26012 gxadd 26015 gxmul 26018 htthlem 26582 atcvati 28051 sinccvglem 30328 midofsegid 30883 outsideofeq 30909 hfun 30957 ordcmp 31119 icoreclin 31772 itgabsnc 32023 dvasin 32040 cvrat 32999 4atlem10 33183 4atlem12 33189 cdleme18d 33873 cdleme22b 33920 cdleme32e 34024 lclkrlem2e 35091 pell1234qrdich 35719 suctrALT 37232 wallispilem3 37939 bgoldbtbnd 38914 |
Copyright terms: Public domain | W3C validator |