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  3637  opth1  4322  onsucelsucexmidlem  4621  reldmtpos  6405  dftpos4  6415  nnm00  6684  xpfi  7102  omp1eomlem  7269  ctmlemr  7283  ctssdclemn0  7285  finomni  7315  indpi  7537  enq0tr  7629  prarloclem3step  7691  distrlem4prl  7779  distrlem4pru  7780  lelttr  8243  nn1suc  9137  nnsub  9157  nn0lt2  9536  uzin  9763  xrlelttr  10010  xlesubadd  10087  fzfig  10660  seq3id  10755  seq3z  10758  faclbnd  10971  facavg  10976  bcval5  10993  hashfzo  11052  swrdccat3blem  11279  iserex  11858  fsum3cvg  11897  fsumf1o  11909  fisumss  11911  fsumcl2lem  11917  fsumadd  11925  fsummulc2  11967  isumsplit  12010  fprodf1o  12107  prodssdc  12108  fprodssdc  12109  fprodmul  12110  absdvdsb  12328  dvdsabsb  12329  dvdsabseq  12366  m1exp1  12420  flodddiv4  12455  gcdaddm  12513  gcdabs1  12518  lcmdvds  12609  prmind2  12650  rpexp  12683  fermltl  12764  pcxnn0cl  12841  pcxcl  12842  pcabs  12857  pcmpt  12874  pockthg  12888  mulgnn0ass  13703  lgseisenlem2  15758  2lgslem1c  15777  trilpolemcl  16435  trilpolemlt1  16439