Theorem mpjaod 861

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 860	. 2 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → 𝜒))
5	1, 4	mpd 15	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∨ wo 848

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 207  df-or 849

This theorem is referenced by:  opth1  5421  onun2  6425  sorpssun  7675  sorpssin  7676  omun  7830  poxp2  8084  poxp3  8091  reldmtpos  8175  dftpos4  8186  oaass  8487  nnawordex  8564  omabs  8578  suplub2  9365  en3lplem2  9523  cantnflt  9582  cantnfp1lem3  9590  ttrclselem2  9636  tcrank  9797  cardaleph  10000  fpwwe2  10555  gchpwdom  10582  grur1  10732  indpi  10819  nn1suc  12185  nnsub  12210  seqid  13998  seqz  14001  faclbnd  14241  facavg  14252  bcval5  14269  hashnnn0genn0  14294  hashfzo  14380  01sqrexlem6  15198  resqrex  15201  absmod0  15254  absz  15262  iserex  15608  fsumf1o  15674  fsumss  15676  fsumcl2lem  15682  fsumadd  15691  fsummulc2  15735  fsumconst  15741  fsumrelem  15759  isumsplit  15794  fprodf1o  15900  fprodss  15902  fprodcl2lem  15904  fprodmul  15914  fproddiv  15915  fprodconst  15932  fprodn0  15933  absdvdsb  16232  dvdsabsb  16233  gcdabs1  16487  bezoutlem1  16497  bezoutlem2  16498  2mulprm  16651  isprm5  16666  pcabs  16835  pockthg  16866  prmreclem5  16880  vdwlem13  16953  0ram  16980  ram0  16982  prmlem0  17065  mulgnn0ass  19075  psgnunilem2  19459  mndodcongi  19507  oddvdsnn0  19508  odnncl  19509  efgredlemb  19710  gsumzres  19873  gsumzcl2  19874  gsumzf1o  19876  gsumzaddlem  19885  gsumconst  19898  gsumzmhm  19901  gsummulglem  19905  gsumzoppg  19908  pgpfac1lem5  20045  ablsimpnosubgd  20070  gsumfsum  21422  zringlpirlem1  21450  mplsubrglem  21991  ordthaus  23358  icccmplem2  24798  metdstri  24826  ioombl  25541  itgabs  25811  dvlip  25970  dvge0  25983  dvivthlem1  25985  dvcnvrelem1  25994  ply1rem  26143  dgrcolem2  26251  quotcan  26288  sinq12ge0  26488  argregt0  26590  argrege0  26591  scvxcvx  26967  bpos1lem  27264  bposlem3  27268  lgseisenlem2  27358  noextendseq  27650  nogt01o  27679  nosupprefixmo  27683  noinfprefixmo  27684  noinfbnd1lem5  27710  noetasuplem4  27719  noetainflem4  27723  n0subs  28374  bdayfinbndlem1  28478  bdayfinlem  28497  bdayfin  28498  frgrregord013  30485  htthlem  31008  atcvati  32477  ccatf1  33029  sinccvglem  35875  midofsegid  36307  outsideofeq  36333  hfun  36381  ordcmp  36650  icoreclin  37684  itgabsnc  38021  dvasin  38036  cvrat  39879  4atlem10  40063  4atlem12  40069  cdleme18d  40752  cdleme22b  40798  cdleme32e  40902  lclkrlem2e  41968  aks4d1p1  42526  pell1234qrdich  43304  onsupnmax  43671  omlimcl2  43685  onexlimgt  43686  onexoegt  43687  onsucf1olem  43713  oege1  43749  cantnfresb  43767  omabs2  43775  tfsconcat0b  43789  clsk1indlem3  44485  suctrALT  45267  wallispilem3  46510  nprmmul2  47985  bgoldbtbnd  48282  reorelicc  49183  infsubc  49532  infsubc2  49533