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  5480  onun2  6492  sorpssun  7750  sorpssin  7751  omun  7909  poxp2  8168  poxp3  8175  reldmtpos  8259  dftpos4  8270  oaass  8599  nnawordex  8675  omabs  8689  suplub2  9501  en3lplem2  9653  cantnflt  9712  cantnfp1lem3  9720  ttrclselem2  9766  tcrank  9924  cardaleph  10129  fpwwe2  10683  gchpwdom  10710  grur1  10860  indpi  10947  nn1suc  12288  nnsub  12310  seqid  14088  seqz  14091  faclbnd  14329  facavg  14340  bcval5  14357  hashnnn0genn0  14382  hashfzo  14468  01sqrexlem6  15286  resqrex  15289  absmod0  15342  absz  15350  iserex  15693  fsumf1o  15759  fsumss  15761  fsumcl2lem  15767  fsumadd  15776  fsummulc2  15820  fsumconst  15826  fsumrelem  15843  isumsplit  15876  fprodf1o  15982  fprodss  15984  fprodcl2lem  15986  fprodmul  15996  fproddiv  15997  fprodconst  16014  fprodn0  16015  absdvdsb  16312  dvdsabsb  16313  gcdabs1  16566  bezoutlem1  16576  bezoutlem2  16577  2mulprm  16730  isprm5  16744  pcabs  16913  pockthg  16944  prmreclem5  16958  vdwlem13  17031  0ram  17058  ram0  17060  prmlem0  17143  mulgnn0ass  19128  psgnunilem2  19513  mndodcongi  19561  oddvdsnn0  19562  odnncl  19563  efgredlemb  19764  gsumzres  19927  gsumzcl2  19928  gsumzf1o  19930  gsumzaddlem  19939  gsumconst  19952  gsumzmhm  19955  gsummulglem  19959  gsumzoppg  19962  pgpfac1lem5  20099  ablsimpnosubgd  20124  gsumfsum  21452  zringlpirlem1  21473  mplsubrglem  22024  ordthaus  23392  icccmplem2  24845  metdstri  24873  ioombl  25600  itgabs  25870  dvlip  26032  dvge0  26045  dvivthlem1  26047  dvcnvrelem1  26056  ply1rem  26205  dgrcolem2  26314  quotcan  26351  sinq12ge0  26550  argregt0  26652  argrege0  26653  scvxcvx  27029  bpos1lem  27326  bposlem3  27330  lgseisenlem2  27420  noextendseq  27712  nogt01o  27741  nosupprefixmo  27745  noinfprefixmo  27746  noinfbnd1lem5  27772  noetasuplem4  27781  noetainflem4  27785  n0subs  28360  frgrregord013  30414  htthlem  30936  atcvati  32405  ccatf1  32933  sinccvglem  35677  midofsegid  36105  outsideofeq  36131  hfun  36179  ordcmp  36448  icoreclin  37358  itgabsnc  37696  dvasin  37711  cvrat  39424  4atlem10  39608  4atlem12  39614  cdleme18d  40297  cdleme22b  40343  cdleme32e  40447  lclkrlem2e  41513  aks4d1p1  42077  pell1234qrdich  42872  onsupnmax  43240  omlimcl2  43254  onexlimgt  43255  onexoegt  43256  onsucf1olem  43283  oege1  43319  cantnfresb  43337  omabs2  43345  tfsconcat0b  43359  clsk1indlem3  44056  suctrALT  44846  wallispilem3  46082  bgoldbtbnd  47796  reorelicc  48631