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  3659  opth1  4354  onsucelsucexmidlem  4653  reldmtpos  6486  dftpos4  6496  nnm00  6765  xpfi  7194  omp1eomlem  7387  ctmlemr  7401  ctssdclemn0  7403  finomni  7433  indpi  7662  enq0tr  7754  prarloclem3step  7816  distrlem4prl  7904  distrlem4pru  7905  lelttr  8367  nn1suc  9261  nnsub  9281  nn0lt2  9665  uzin  9893  xrlelttr  10145  xlesubadd  10222  fzfig  10799  seq3id  10894  seq3z  10897  faclbnd  11111  facavg  11116  bcval5  11133  hashfzo  11195  swrdccat3blem  11439  iserex  12032  fsum3cvg  12072  fsumf1o  12084  fisumss  12086  fsumcl2lem  12092  fsumadd  12100  fsummulc2  12142  isumsplit  12185  fprodf1o  12282  prodssdc  12283  fprodssdc  12284  fprodmul  12285  absdvdsb  12503  dvdsabsb  12504  dvdsabseq  12541  m1exp1  12595  flodddiv4  12630  gcdaddm  12688  gcdabs1  12693  lcmdvds  12784  prmind2  12825  rpexp  12858  fermltl  12939  pcxnn0cl  13016  pcxcl  13017  pcabs  13032  pcmpt  13049  pockthg  13063  mulgnn0ass  13896  lgseisenlem2  15993  2lgslem1c  16012  trilpolemcl  16870  trilpolemlt1  16874