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  3656  opth1  4351  onsucelsucexmidlem  4650  reldmtpos  6483  dftpos4  6493  nnm00  6762  xpfi  7191  omp1eomlem  7384  ctmlemr  7398  ctssdclemn0  7400  finomni  7430  indpi  7653  enq0tr  7745  prarloclem3step  7807  distrlem4prl  7895  distrlem4pru  7896  lelttr  8358  nn1suc  9252  nnsub  9272  nn0lt2  9655  uzin  9883  xrlelttr  10135  xlesubadd  10212  fzfig  10788  seq3id  10883  seq3z  10886  faclbnd  11099  facavg  11104  bcval5  11121  hashfzo  11182  swrdccat3blem  11424  iserex  12017  fsum3cvg  12057  fsumf1o  12069  fisumss  12071  fsumcl2lem  12077  fsumadd  12085  fsummulc2  12127  isumsplit  12170  fprodf1o  12267  prodssdc  12268  fprodssdc  12269  fprodmul  12270  absdvdsb  12488  dvdsabsb  12489  dvdsabseq  12526  m1exp1  12580  flodddiv4  12615  gcdaddm  12673  gcdabs1  12678  lcmdvds  12769  prmind2  12810  rpexp  12843  fermltl  12924  pcxnn0cl  13001  pcxcl  13002  pcabs  13017  pcmpt  13034  pockthg  13048  mulgnn0ass  13864  lgseisenlem2  15931  2lgslem1c  15950  trilpolemcl  16808  trilpolemlt1  16812