Theorem mpjaod 866

Description: Eliminate a disjunction in a deduction. (Contributed by Mario Carneiro, 29-May-2016.)

Hypotheses

Ref	Expression
jaod.1	⊢ (𝜑 → (𝜓 → 𝜒))
jaod.2	⊢ (𝜑 → (𝜃 → 𝜒))
jaod.3	⊢ (𝜑 → (𝜓 ∨ 𝜃))

Assertion

Ref	Expression
mpjaod	⊢ (𝜑 → 𝜒)

Proof of Theorem mpjaod

Step	Hyp	Ref	Expression
1		jaod.3	. 2 ⊢ (𝜑 → (𝜓 ∨ 𝜃))
2		jaod.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3		jaod.2	. . 3 ⊢ (𝜑 → (𝜃 → 𝜒))
4	2, 3	jaod 865	. 2 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → 𝜒))
5	1, 4	mpd 15	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∨ wo 853

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 208  df-or 854

This theorem is referenced by:  opth1  5422  onun2  6427  sorpssun  7680  sorpssin  7681  omun  7835  poxp2  8090  poxp3  8097  reldmtpos  8181  dftpos4  8192  oaass  8493  nnawordex  8570  omabs  8584  suplub2  9371  en3lplem2  9532  cantnflt  9591  cantnfp1lem3  9599  ttrclselem2  9645  tcrank  9806  cardaleph  10009  fpwwe2  10564  gchpwdom  10591  grur1  10741  indpi  10828  nn1suc  12194  nnsub  12219  seqid  14007  seqz  14010  faclbnd  14250  facavg  14261  bcval5  14278  hashnnn0genn0  14303  hashfzo  14389  01sqrexlem6  15207  resqrex  15210  absmod0  15263  absz  15271  iserex  15617  fsumf1o  15683  fsumss  15685  fsumcl2lem  15691  fsumadd  15700  fsummulc2  15744  fsumconst  15750  fsumrelem  15768  isumsplit  15803  fprodf1o  15909  fprodss  15911  fprodcl2lem  15913  fprodmul  15923  fproddiv  15924  fprodconst  15941  fprodn0  15942  absdvdsb  16241  dvdsabsb  16242  gcdabs1  16496  bezoutlem1  16506  bezoutlem2  16507  2mulprm  16660  isprm5  16675  pcabs  16844  pockthg  16875  prmreclem5  16889  vdwlem13  16962  0ram  16989  ram0  16991  prmlem0  17074  mulgnn0ass  19084  psgnunilem2  19468  mndodcongi  19516  oddvdsnn0  19517  odnncl  19518  efgredlemb  19719  gsumzres  19882  gsumzcl2  19883  gsumzf1o  19885  gsumzaddlem  19894  gsumconst  19907  gsumzmhm  19910  gsummulglem  19914  gsumzoppg  19917  pgpfac1lem5  20054  ablsimpnosubgd  20079  gsumfsum  21416  zringlpirlem1  21444  mplsubrglem  21985  ordthaus  23374  icccmplem2  24814  metdstri  24842  ioombl  25557  itgabs  25827  dvlip  25985  dvge0  25998  dvivthlem1  26000  dvcnvrelem1  26009  ply1rem  26156  dgrcolem2  26264  quotcan  26300  sinq12ge0  26497  argregt0  26599  argrege0  26600  scvxcvx  26974  bpos1lem  27270  bposlem3  27274  lgseisenlem2  27364  noextendseq  27656  nogt01o  27685  nosupprefixmo  27689  noinfprefixmo  27690  noinfbnd1lem5  27716  noetasuplem4  27725  noetainflem4  27729  n0subs  28380  bdayfinbndlem1  28484  bdayfinlem  28503  bdayfin  28504  frgrregord013  30490  htthlem  31013  atcvati  32482  ccatf1  33035  sinccvglem  35901  midofsegid  36333  outsideofeq  36359  hfun  36407  ordcmp  36676  icoreclin  37720  itgabsnc  38057  dvasin  38072  cvrat  39915  4atlem10  40099  4atlem12  40105  cdleme18d  40788  cdleme22b  40834  cdleme32e  40938  lclkrlem2e  42004  aks4d1p1  42562  pell1234qrdich  43307  onsupnmax  43674  omlimcl2  43688  onexlimgt  43689  onexoegt  43690  onsucf1olem  43716  oege1  43752  cantnfresb  43770  omabs2  43778  tfsconcat0b  43792  clsk1indlem3  44488  suctrALT  45270  wallispilem3  46511  nprmmul2  48004  bgoldbtbnd  48301  reorelicc  49202  infsubc  49551  infsubc2  49552