Theorem mpjaod 725

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

Syntax hints:   → wi 4   ∨ wo 715

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 716

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ifbothdc  3640  opth1  4328  onsucelsucexmidlem  4627  reldmtpos  6419  dftpos4  6429  nnm00  6698  xpfi  7124  omp1eomlem  7293  ctmlemr  7307  ctssdclemn0  7309  finomni  7339  indpi  7562  enq0tr  7654  prarloclem3step  7716  distrlem4prl  7804  distrlem4pru  7805  lelttr  8268  nn1suc  9162  nnsub  9182  nn0lt2  9561  uzin  9789  xrlelttr  10041  xlesubadd  10118  fzfig  10693  seq3id  10788  seq3z  10791  faclbnd  11004  facavg  11009  bcval5  11026  hashfzo  11087  swrdccat3blem  11321  iserex  11901  fsum3cvg  11941  fsumf1o  11953  fisumss  11955  fsumcl2lem  11961  fsumadd  11969  fsummulc2  12011  isumsplit  12054  fprodf1o  12151  prodssdc  12152  fprodssdc  12153  fprodmul  12154  absdvdsb  12372  dvdsabsb  12373  dvdsabseq  12410  m1exp1  12464  flodddiv4  12499  gcdaddm  12557  gcdabs1  12562  lcmdvds  12653  prmind2  12694  rpexp  12727  fermltl  12808  pcxnn0cl  12885  pcxcl  12886  pcabs  12901  pcmpt  12918  pockthg  12932  mulgnn0ass  13747  lgseisenlem2  15803  2lgslem1c  15822  trilpolemcl  16662  trilpolemlt1  16666