Theorem mpjaod 874

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

This proof depends on syntax axioms:   → wi 4   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862

This theorem is used by:  opth1  5448  onun2  6491  sorpssun  7770  sorpssin  7771  omun  7923  poxp2  8187  poxp3  8194  reldmtpos  8279  dftpos4  8290  oaass  8597  nnawordex  8674  omabs  8688  suplub2  9480  en3lplem2  9641  cantnflt  9700  cantnfp1lem3  9708  ttrclselem2  9754  tcrank  9928  hfunOLD  9946  cardaleph  10195  fpwwe2  10755  gchpwdom  10782  grur1  10932  indpi  11019  nn1suc  12384  nnsub  12409  seqid  14217  seqz  14220  faclbnd  14461  facavg  14472  bcval5  14489  hashnnn0genn0  14514  hashfzo  14601  ccatf1  14763  01sqrexlem6  15443  resqrex  15446  absmod0  15499  absz  15507  iserex  15853  fsumf1o  15918  fsumss  15920  fsumcl2lem  15926  fsumadd  15935  fsummulc2  15979  fsumconst  15985  fsumrelem  16003  isumsplit  16038  fprodf1o  16142  fprodss  16144  fprodcl2lem  16146  fprodmul  16156  fproddiv  16157  fprodconst  16174  fprodn0  16175  absdvdsb  16473  dvdsabsb  16474  gcdabs1  16731  bezoutlem1  16741  bezoutlem2  16742  2mulprm  16897  isprm5  16912  pcabs  17082  pockthg  17113  prmreclem5  17127  vdwlem13  17200  0ram  17227  ram0  17229  prmlem0  17312  mulgnn0ass  19349  psgnunilem2  19739  mndodcongi  19787  oddvdsnn0  19788  odnncl  19789  efgredlemb  19990  gsumzres  20153  gsumzcl2  20154  gsumzf1o  20156  gsumzaddlem  20165  gsumconst  20178  gsumzmhm  20181  gsummulglem  20185  gsumzoppg  20188  pgpfac1lem5  20325  ablsimpnosubgd  20350  gsumfsum  21770  zringlpirlem1  21798  mplsubrglem  22341  ordthaus  23732  icccmplem2  25173  metdstri  25201  ioombl  25916  itgabs  26185  dvlip  26343  dvge0  26356  dvivthlem1  26358  dvcnvrelem1  26367  ply1rem  26514  dgrcolem2  26623  quotcan  26662  sinq12ge0  26867  argregt0  26968  argrege0  26969  scvxcvx  27343  bpos1lem  27639  bposlem3  27643  lgseisenlem2  27733  fltoprm  28025  noextendseq  28054  nogt01o  28083  nosupprefixmo  28087  noinfprefixmo  28088  noinfbnd1lem5  28114  noetasuplem4  28123  noetainflem4  28127  n0subs  28779  bdayfinbndlem1  28883  bdayfinlem  28902  bdayfin  28903  frgrregord013  31026  htthlem  31549  atcvati  33018  maxssj0  36006  sinccvglem  36604  mirimanoffr  36627  mirimanofffr  36629  midofsegid  37047  outsideofeq  37073  ordcmp  37413  icoreclin  38472  itgabsnc  38799  dvasin  38814  cvrat  40671  4atlem10  40855  4atlem12  40861  cdleme18d  41544  cdleme22b  41590  cdleme32e  41694  lclkrlem2e  42760  aks4d1p1  43318  pell1234qrdich  44061  onsupnmax  44422  omlimcl2  44436  onexlimgt  44437  onexoegt  44438  onsucf1olem  44464  oege1  44500  cantnfresb  44518  omabs2  44526  tfsconcat0b  44540  clsk1indlem3  45235  suctrALT  45999  wallispilem3  47282  nprmmul2  48815  bgoldbtbnd  49112  reorelicc  50027  infsubc  50379  infsubc2  50380