Theorem mpjaod 723

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

Syntax hints:   → wi 4   ∨ wo 713

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 714

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ifbothdc  3637  opth1  4323  onsucelsucexmidlem  4622  reldmtpos  6410  dftpos4  6420  nnm00  6689  xpfi  7110  omp1eomlem  7277  ctmlemr  7291  ctssdclemn0  7293  finomni  7323  indpi  7545  enq0tr  7637  prarloclem3step  7699  distrlem4prl  7787  distrlem4pru  7788  lelttr  8251  nn1suc  9145  nnsub  9165  nn0lt2  9544  uzin  9772  xrlelttr  10019  xlesubadd  10096  fzfig  10669  seq3id  10764  seq3z  10767  faclbnd  10980  facavg  10985  bcval5  11002  hashfzo  11062  swrdccat3blem  11292  iserex  11871  fsum3cvg  11910  fsumf1o  11922  fisumss  11924  fsumcl2lem  11930  fsumadd  11938  fsummulc2  11980  isumsplit  12023  fprodf1o  12120  prodssdc  12121  fprodssdc  12122  fprodmul  12123  absdvdsb  12341  dvdsabsb  12342  dvdsabseq  12379  m1exp1  12433  flodddiv4  12468  gcdaddm  12526  gcdabs1  12531  lcmdvds  12622  prmind2  12663  rpexp  12696  fermltl  12777  pcxnn0cl  12854  pcxcl  12855  pcabs  12870  pcmpt  12887  pockthg  12901  mulgnn0ass  13716  lgseisenlem2  15771  2lgslem1c  15790  trilpolemcl  16519  trilpolemlt1  16523