Theorem mpjaod 725

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

Syntax hints:   → wi 4   ∨ wo 715

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 716

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ifbothdc  3641  opth1  4330  onsucelsucexmidlem  4629  reldmtpos  6424  dftpos4  6434  nnm00  6703  xpfi  7129  omp1eomlem  7298  ctmlemr  7312  ctssdclemn0  7314  finomni  7344  indpi  7567  enq0tr  7659  prarloclem3step  7721  distrlem4prl  7809  distrlem4pru  7810  lelttr  8273  nn1suc  9167  nnsub  9187  nn0lt2  9566  uzin  9794  xrlelttr  10046  xlesubadd  10123  fzfig  10698  seq3id  10793  seq3z  10796  faclbnd  11009  facavg  11014  bcval5  11031  hashfzo  11092  swrdccat3blem  11329  iserex  11922  fsum3cvg  11962  fsumf1o  11974  fisumss  11976  fsumcl2lem  11982  fsumadd  11990  fsummulc2  12032  isumsplit  12075  fprodf1o  12172  prodssdc  12173  fprodssdc  12174  fprodmul  12175  absdvdsb  12393  dvdsabsb  12394  dvdsabseq  12431  m1exp1  12485  flodddiv4  12520  gcdaddm  12578  gcdabs1  12583  lcmdvds  12674  prmind2  12715  rpexp  12748  fermltl  12829  pcxnn0cl  12906  pcxcl  12907  pcabs  12922  pcmpt  12939  pockthg  12953  mulgnn0ass  13768  lgseisenlem2  15829  2lgslem1c  15848  trilpolemcl  16708  trilpolemlt1  16712