Theorem mpjaod 671

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

Syntax hints:   → wi 4   ∨ wo 662

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 663

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  ifbothdc  3388  opth1  3999  onsucelsucexmidlem  4280  reldmtpos  5902  dftpos4  5912  nnm00  6168  indpi  6594  enq0tr  6686  prarloclem3step  6748  distrlem4prl  6836  distrlem4pru  6837  lelttr  7266  nn1suc  8125  nnsub  8144  nn0lt2  8510  uzin  8732  xrlelttr  8952  fzfig  9512  iseqid  9563  iseqz  9566  expival  9575  faclbnd  9765  facavg  9770  ibcval5  9787  iiserex  10315  fisumcvg  10338  absdvdsb  10358  dvdsabsb  10359  dvdsabseq  10392  m1exp1  10445  flodddiv4  10478  gcdaddm  10519  gcdabs1  10524  lcmdvds  10605  prmind2  10646  rpexp  10676