Theorem mpjaod 673

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

Syntax hints:   → wi 4   ∨ wo 664

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 665

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  ifbothdc  3419  opth1  4054  onsucelsucexmidlem  4335  reldmtpos  6000  dftpos4  6010  nnm00  6268  xpfi  6619  finomni  6775  indpi  6880  enq0tr  6972  prarloclem3step  7034  distrlem4prl  7122  distrlem4pru  7123  lelttr  7552  nn1suc  8413  nnsub  8432  nn0lt2  8798  uzin  9020  xrlelttr  9240  fzfig  9802  iseqid  9904  iseqz  9907  faclbnd  10113  facavg  10118  ibcval5  10135  hashfzo  10194  iserex  10690  fisumcvg  10729  fsumf1o  10744  fisumss  10746  fsumcl2lem  10753  fsumadd  10761  fsummulc2  10803  isumsplit  10845  absdvdsb  10894  dvdsabsb  10895  dvdsabseq  10928  m1exp1  10981  flodddiv4  11014  gcdaddm  11055  gcdabs1  11060  lcmdvds  11141  prmind2  11182  rpexp  11212