Theorem mpjaod 720

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

Syntax hints:   → wi 4   ∨ wo 710

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 711

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ifbothdc  3606  opth1  4284  onsucelsucexmidlem  4581  reldmtpos  6346  dftpos4  6356  nnm00  6623  xpfi  7036  omp1eomlem  7203  ctmlemr  7217  ctssdclemn0  7219  finomni  7249  indpi  7462  enq0tr  7554  prarloclem3step  7616  distrlem4prl  7704  distrlem4pru  7705  lelttr  8168  nn1suc  9062  nnsub  9082  nn0lt2  9461  uzin  9688  xrlelttr  9935  xlesubadd  10012  fzfig  10582  seq3id  10677  seq3z  10680  faclbnd  10893  facavg  10898  bcval5  10915  hashfzo  10974  iserex  11694  fsum3cvg  11733  fsumf1o  11745  fisumss  11747  fsumcl2lem  11753  fsumadd  11761  fsummulc2  11803  isumsplit  11846  fprodf1o  11943  prodssdc  11944  fprodssdc  11945  fprodmul  11946  absdvdsb  12164  dvdsabsb  12165  dvdsabseq  12202  m1exp1  12256  flodddiv4  12291  gcdaddm  12349  gcdabs1  12354  lcmdvds  12445  prmind2  12486  rpexp  12519  fermltl  12600  pcxnn0cl  12677  pcxcl  12678  pcabs  12693  pcmpt  12710  pockthg  12724  mulgnn0ass  13538  lgseisenlem2  15592  2lgslem1c  15611  trilpolemcl  16050  trilpolemlt1  16054