Theorem mpjaod 707

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

Syntax hints:   → wi 4   ∨ wo 697

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ifbothdc  3499  opth1  4153  onsucelsucexmidlem  4439  reldmtpos  6143  dftpos4  6153  nnm00  6418  xpfi  6811  omp1eomlem  6972  ctmlemr  6986  ctssdclemn0  6988  finomni  7005  indpi  7143  enq0tr  7235  prarloclem3step  7297  distrlem4prl  7385  distrlem4pru  7386  lelttr  7845  nn1suc  8732  nnsub  8752  nn0lt2  9125  uzin  9351  xrlelttr  9582  xlesubadd  9659  fzfig  10196  seq3id  10274  seq3z  10277  faclbnd  10480  facavg  10485  bcval5  10502  hashfzo  10561  iserex  11101  fsum3cvg  11139  fsumf1o  11152  fisumss  11154  fsumcl2lem  11160  fsumadd  11168  fsummulc2  11210  isumsplit  11253  absdvdsb  11500  dvdsabsb  11501  dvdsabseq  11534  m1exp1  11587  flodddiv4  11620  gcdaddm  11661  gcdabs1  11666  lcmdvds  11749  prmind2  11790  rpexp  11820  trilpolemcl  13219  trilpolemlt1  13223