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  4378  onsucelsucexmidlem  4678  reldmtpos  6528  dftpos4  6538  nnm00  6807  xpfi  7244  omp1eomlem  7441  ctmlemr  7455  ctssdclemn0  7457  finomni  7487  indpi  7716  enq0tr  7808  prarloclem3step  7870  distrlem4prl  7958  distrlem4pru  7959  lelttr  8421  nn1suc  9333  nnsub  9353  nn0lt2  9739  uzin  9972  xrlelttr  10226  xlesubadd  10303  fzfig  10889  seq3id  10984  seq3z  10987  faclbnd  11202  facavg  11207  bcval5  11224  hashfzo  11286  swrdccat3blem  11534  iserex  12131  fsum3cvg  12171  fsumf1o  12183  fisumss  12185  fsumcl2lem  12191  fsumadd  12199  fsummulc2  12241  isumsplit  12284  fprodf1o  12381  prodssdc  12382  fprodssdc  12383  fprodmul  12384  absdvdsb  12602  dvdsabsb  12603  dvdsabseq  12640  m1exp1  12694  flodddiv4  12729  gcdaddm  12787  gcdabs1  12792  lcmdvds  12883  prmind2  12924  rpexp  12958  fermltl  13042  pcxnn0cl  13119  pcxcl  13120  pcabs  13135  pcmpt  13152  pockthg  13166  prmlem0  13250  prmlem1a  13251  mulgnn0ass  14021  chtublem  16307  bpos1lem  16321  bposlem1  16323  bposlem3  16325  lgseisenlem2  16407  2lgslem1c  16426  trilpolemcl  17305  trilpolemlt1  17309