Theorem mpjaod 707

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

Syntax hints:   → wi 4   ∨ wo 697

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ifbothdc  3504  opth1  4158  onsucelsucexmidlem  4444  reldmtpos  6150  dftpos4  6160  nnm00  6425  xpfi  6818  omp1eomlem  6979  ctmlemr  6993  ctssdclemn0  6995  finomni  7012  indpi  7150  enq0tr  7242  prarloclem3step  7304  distrlem4prl  7392  distrlem4pru  7393  lelttr  7852  nn1suc  8739  nnsub  8759  nn0lt2  9132  uzin  9358  xrlelttr  9589  xlesubadd  9666  fzfig  10203  seq3id  10281  seq3z  10284  faclbnd  10487  facavg  10492  bcval5  10509  hashfzo  10568  iserex  11108  fsum3cvg  11147  fsumf1o  11159  fisumss  11161  fsumcl2lem  11167  fsumadd  11175  fsummulc2  11217  isumsplit  11260  absdvdsb  11511  dvdsabsb  11512  dvdsabseq  11545  m1exp1  11598  flodddiv4  11631  gcdaddm  11672  gcdabs1  11677  lcmdvds  11760  prmind2  11801  rpexp  11831  trilpolemcl  13230  trilpolemlt1  13234