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 ⊢ (𝜑 → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∨ wo 720

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721

This proof depends on definitions:  df-bi 117

This theorem is used by:  ifbothdc  3675  opth1  4376  onsucelsucexmidlem  4676  reldmtpos  6524  dftpos4  6534  nnm00  6803  xpfi  7239  omp1eomlem  7434  ctmlemr  7448  ctssdclemn0  7450  finomni  7480  indpi  7709  enq0tr  7801  prarloclem3step  7863  distrlem4prl  7951  distrlem4pru  7952  lelttr  8414  nn1suc  9324  nnsub  9344  nn0lt2  9729  uzin  9957  xrlelttr  10210  xlesubadd  10287  fzfig  10869  seq3id  10964  seq3z  10967  faclbnd  11181  facavg  11186  bcval5  11203  hashfzo  11265  swrdccat3blem  11513  iserex  12107  fsum3cvg  12147  fsumf1o  12159  fisumss  12161  fsumcl2lem  12167  fsumadd  12175  fsummulc2  12217  isumsplit  12260  fprodf1o  12357  prodssdc  12358  fprodssdc  12359  fprodmul  12360  absdvdsb  12578  dvdsabsb  12579  dvdsabseq  12616  m1exp1  12670  flodddiv4  12705  gcdaddm  12763  gcdabs1  12768  lcmdvds  12859  prmind2  12900  rpexp  12933  fermltl  13014  pcxnn0cl  13091  pcxcl  13092  pcabs  13107  pcmpt  13124  pockthg  13138  mulgnn0ass  13963  lgseisenlem2  16202  2lgslem1c  16221  trilpolemcl  17098  trilpolemlt1  17102