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  5443  onun2  6462  sorpssun  7729  sorpssin  7730  omun  7882  poxp2  8138  poxp3  8145  reldmtpos  8229  dftpos4  8240  oaass  8547  nnawordex  8624  omabs  8638  suplub2  9431  en3lplem2  9592  cantnflt  9651  cantnfp1lem3  9659  ttrclselem2  9705  tcrank  9874  hfunOLD  9891  cardaleph  10140  fpwwe2  10700  gchpwdom  10727  grur1  10877  indpi  10964  nn1suc  12327  nnsub  12352  seqid  14159  seqz  14162  faclbnd  14402  facavg  14413  bcval5  14430  hashnnn0genn0  14455  hashfzo  14542  ccatf1  14704  01sqrexlem6  15382  resqrex  15385  absmod0  15438  absz  15446  iserex  15792  fsumf1o  15857  fsumss  15859  fsumcl2lem  15865  fsumadd  15874  fsummulc2  15918  fsumconst  15924  fsumrelem  15942  isumsplit  15977  fprodf1o  16081  fprodss  16083  fprodcl2lem  16085  fprodmul  16095  fproddiv  16096  fprodconst  16113  fprodn0  16114  absdvdsb  16412  dvdsabsb  16413  gcdabs1  16667  bezoutlem1  16677  bezoutlem2  16678  2mulprm  16831  isprm5  16846  pcabs  17015  pockthg  17046  prmreclem5  17060  vdwlem13  17133  0ram  17160  ram0  17162  prmlem0  17245  mulgnn0ass  19282  psgnunilem2  19671  mndodcongi  19719  oddvdsnn0  19720  odnncl  19721  efgredlemb  19922  gsumzres  20085  gsumzcl2  20086  gsumzf1o  20088  gsumzaddlem  20097  gsumconst  20110  gsumzmhm  20113  gsummulglem  20117  gsumzoppg  20120  pgpfac1lem5  20257  ablsimpnosubgd  20282  gsumfsum  21702  zringlpirlem1  21730  mplsubrglem  22273  ordthaus  23664  icccmplem2  25105  metdstri  25133  ioombl  25848  itgabs  26117  dvlip  26275  dvge0  26288  dvivthlem1  26290  dvcnvrelem1  26299  ply1rem  26446  dgrcolem2  26555  quotcan  26596  sinq12ge0  26801  argregt0  26902  argrege0  26903  scvxcvx  27277  bpos1lem  27573  bposlem3  27577  lgseisenlem2  27667  noextendseq  27958  nogt01o  27987  nosupprefixmo  27991  noinfprefixmo  27992  noinfbnd1lem5  28018  noetasuplem4  28027  noetainflem4  28031  n0subs  28683  bdayfinbndlem1  28787  bdayfinlem  28806  bdayfin  28807  frgrregord013  30930  htthlem  31453  atcvati  32922  sinccvglem  36358  midofsegid  36791  outsideofeq  36817  ordcmp  37157  icoreclin  38200  itgabsnc  38527  dvasin  38542  cvrat  40399  4atlem10  40583  4atlem12  40589  cdleme18d  41272  cdleme22b  41318  cdleme32e  41422  lclkrlem2e  42488  aks4d1p1  43046  pell1234qrdich  43806  onsupnmax  44173  omlimcl2  44187  onexlimgt  44188  onexoegt  44189  onsucf1olem  44215  oege1  44251  cantnfresb  44269  omabs2  44277  tfsconcat0b  44291  clsk1indlem3  44987  suctrALT  45752  wallispilem3  46999  nprmmul2  48532  bgoldbtbnd  48829  reorelicc  49744  infsubc  50090  infsubc2  50091