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  3595  opth1  4270  onsucelsucexmidlem  4566  reldmtpos  6320  dftpos4  6330  nnm00  6597  xpfi  7002  omp1eomlem  7169  ctmlemr  7183  ctssdclemn0  7185  finomni  7215  indpi  7428  enq0tr  7520  prarloclem3step  7582  distrlem4prl  7670  distrlem4pru  7671  lelttr  8134  nn1suc  9028  nnsub  9048  nn0lt2  9426  uzin  9653  xrlelttr  9900  xlesubadd  9977  fzfig  10541  seq3id  10636  seq3z  10639  faclbnd  10852  facavg  10857  bcval5  10874  hashfzo  10933  iserex  11523  fsum3cvg  11562  fsumf1o  11574  fisumss  11576  fsumcl2lem  11582  fsumadd  11590  fsummulc2  11632  isumsplit  11675  fprodf1o  11772  prodssdc  11773  fprodssdc  11774  fprodmul  11775  absdvdsb  11993  dvdsabsb  11994  dvdsabseq  12031  m1exp1  12085  flodddiv4  12120  gcdaddm  12178  gcdabs1  12183  lcmdvds  12274  prmind2  12315  rpexp  12348  fermltl  12429  pcxnn0cl  12506  pcxcl  12507  pcabs  12522  pcmpt  12539  pockthg  12553  mulgnn0ass  13366  lgseisenlem2  15398  2lgslem1c  15417  trilpolemcl  15772  trilpolemlt1  15776