Theorem mpjaod 722

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

Syntax hints:   → wi 4   ∨ wo 712

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 713

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ifbothdc  3617  opth1  4301  onsucelsucexmidlem  4598  reldmtpos  6369  dftpos4  6379  nnm00  6646  xpfi  7062  omp1eomlem  7229  ctmlemr  7243  ctssdclemn0  7245  finomni  7275  indpi  7497  enq0tr  7589  prarloclem3step  7651  distrlem4prl  7739  distrlem4pru  7740  lelttr  8203  nn1suc  9097  nnsub  9117  nn0lt2  9496  uzin  9723  xrlelttr  9970  xlesubadd  10047  fzfig  10619  seq3id  10714  seq3z  10717  faclbnd  10930  facavg  10935  bcval5  10952  hashfzo  11011  swrdccat3blem  11237  iserex  11816  fsum3cvg  11855  fsumf1o  11867  fisumss  11869  fsumcl2lem  11875  fsumadd  11883  fsummulc2  11925  isumsplit  11968  fprodf1o  12065  prodssdc  12066  fprodssdc  12067  fprodmul  12068  absdvdsb  12286  dvdsabsb  12287  dvdsabseq  12324  m1exp1  12378  flodddiv4  12413  gcdaddm  12471  gcdabs1  12476  lcmdvds  12567  prmind2  12608  rpexp  12641  fermltl  12722  pcxnn0cl  12799  pcxcl  12800  pcabs  12815  pcmpt  12832  pockthg  12846  mulgnn0ass  13661  lgseisenlem2  15715  2lgslem1c  15734  trilpolemcl  16316  trilpolemlt1  16320