Theorem mpjaod 723

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

Syntax hints:   → wi 4   ∨ wo 713

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 714

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ifbothdc  3638  opth1  4326  onsucelsucexmidlem  4625  reldmtpos  6414  dftpos4  6424  nnm00  6693  xpfi  7119  omp1eomlem  7287  ctmlemr  7301  ctssdclemn0  7303  finomni  7333  indpi  7555  enq0tr  7647  prarloclem3step  7709  distrlem4prl  7797  distrlem4pru  7798  lelttr  8261  nn1suc  9155  nnsub  9175  nn0lt2  9554  uzin  9782  xrlelttr  10034  xlesubadd  10111  fzfig  10685  seq3id  10780  seq3z  10783  faclbnd  10996  facavg  11001  bcval5  11018  hashfzo  11079  swrdccat3blem  11313  iserex  11893  fsum3cvg  11932  fsumf1o  11944  fisumss  11946  fsumcl2lem  11952  fsumadd  11960  fsummulc2  12002  isumsplit  12045  fprodf1o  12142  prodssdc  12143  fprodssdc  12144  fprodmul  12145  absdvdsb  12363  dvdsabsb  12364  dvdsabseq  12401  m1exp1  12455  flodddiv4  12490  gcdaddm  12548  gcdabs1  12553  lcmdvds  12644  prmind2  12685  rpexp  12718  fermltl  12799  pcxnn0cl  12876  pcxcl  12877  pcabs  12892  pcmpt  12909  pockthg  12923  mulgnn0ass  13738  lgseisenlem2  15793  2lgslem1c  15812  trilpolemcl  16591  trilpolemlt1  16595