Theorem mpjaod 719

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

Syntax hints:   → wi 4   ∨ wo 709

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 710

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ifbothdc  3582  opth1  4254  onsucelsucexmidlem  4546  reldmtpos  6279  dftpos4  6289  nnm00  6556  xpfi  6959  omp1eomlem  7124  ctmlemr  7138  ctssdclemn0  7140  finomni  7169  indpi  7372  enq0tr  7464  prarloclem3step  7526  distrlem4prl  7614  distrlem4pru  7615  lelttr  8077  nn1suc  8969  nnsub  8989  nn0lt2  9365  uzin  9592  xrlelttr  9838  xlesubadd  9915  fzfig  10463  seq3id  10541  seq3z  10544  faclbnd  10756  facavg  10761  bcval5  10778  hashfzo  10837  iserex  11382  fsum3cvg  11421  fsumf1o  11433  fisumss  11435  fsumcl2lem  11441  fsumadd  11449  fsummulc2  11491  isumsplit  11534  fprodf1o  11631  prodssdc  11632  fprodssdc  11633  fprodmul  11634  absdvdsb  11851  dvdsabsb  11852  dvdsabseq  11888  m1exp1  11941  flodddiv4  11974  gcdaddm  12020  gcdabs1  12025  lcmdvds  12114  prmind2  12155  rpexp  12188  fermltl  12269  pcxnn0cl  12345  pcxcl  12346  pcabs  12361  pcmpt  12378  pockthg  12392  mulgnn0ass  13115  lgseisenlem2  14929  trilpolemcl  15264  trilpolemlt1  15268