Theorem mpjaod 726

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

Syntax hints:   → wi 4   ∨ wo 716

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ifbothdc  3661  opth1  4357  onsucelsucexmidlem  4656  reldmtpos  6497  dftpos4  6507  nnm00  6776  xpfi  7205  omp1eomlem  7398  ctmlemr  7412  ctssdclemn0  7414  finomni  7444  indpi  7673  enq0tr  7765  prarloclem3step  7827  distrlem4prl  7915  distrlem4pru  7916  lelttr  8378  nn1suc  9276  nnsub  9296  nn0lt2  9680  uzin  9908  xrlelttr  10161  xlesubadd  10238  fzfig  10819  seq3id  10914  seq3z  10917  faclbnd  11131  facavg  11136  bcval5  11153  hashfzo  11215  swrdccat3blem  11459  iserex  12052  fsum3cvg  12092  fsumf1o  12104  fisumss  12106  fsumcl2lem  12112  fsumadd  12120  fsummulc2  12162  isumsplit  12205  fprodf1o  12302  prodssdc  12303  fprodssdc  12304  fprodmul  12305  absdvdsb  12523  dvdsabsb  12524  dvdsabseq  12561  m1exp1  12615  flodddiv4  12650  gcdaddm  12708  gcdabs1  12713  lcmdvds  12804  prmind2  12845  rpexp  12878  fermltl  12959  pcxnn0cl  13036  pcxcl  13037  pcabs  13052  pcmpt  13069  pockthg  13083  mulgnn0ass  13914  lgseisenlem2  16073  2lgslem1c  16092  trilpolemcl  16960  trilpolemlt1  16964