Theorem mpjaod 730

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

Syntax hints:   → wi 4   ∨ wo 720

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 721

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ifbothdc  3675  opth1  4374  onsucelsucexmidlem  4674  reldmtpos  6518  dftpos4  6528  nnm00  6797  xpfi  7233  omp1eomlem  7428  ctmlemr  7442  ctssdclemn0  7444  finomni  7474  indpi  7703  enq0tr  7795  prarloclem3step  7857  distrlem4prl  7945  distrlem4pru  7946  lelttr  8408  nn1suc  9306  nnsub  9326  nn0lt2  9710  uzin  9938  xrlelttr  10191  xlesubadd  10268  fzfig  10850  seq3id  10945  seq3z  10948  faclbnd  11162  facavg  11167  bcval5  11184  hashfzo  11246  swrdccat3blem  11494  iserex  12088  fsum3cvg  12128  fsumf1o  12140  fisumss  12142  fsumcl2lem  12148  fsumadd  12156  fsummulc2  12198  isumsplit  12241  fprodf1o  12338  prodssdc  12339  fprodssdc  12340  fprodmul  12341  absdvdsb  12559  dvdsabsb  12560  dvdsabseq  12597  m1exp1  12651  flodddiv4  12686  gcdaddm  12744  gcdabs1  12749  lcmdvds  12840  prmind2  12881  rpexp  12914  fermltl  12995  pcxnn0cl  13072  pcxcl  13073  pcabs  13088  pcmpt  13105  pockthg  13119  mulgnn0ass  13944  lgseisenlem2  16173  2lgslem1c  16192  trilpolemcl  17060  trilpolemlt1  17064