Theorem mpjaod 730

Description: Eliminate a disjunction in a deduction. (Contributed by Mario Carneiro, 29-May-2016.)

Hypotheses

Ref	Expression
jaod.1	|- ( ph -> ( ps -> ch ) )
jaod.2	|- ( ph -> ( th -> ch ) )
jaod.3	|- ( ph -> ( ps \/ th ) )

Assertion

Ref	Expression
mpjaod	|- ( ph -> ch )

Proof of Theorem mpjaod

Step	Hyp	Ref	Expression
1		jaod.3	. 2 |- ( ph -> ( ps \/ th ) )
2		jaod.1	. . 3 |- ( ph -> ( ps -> ch ) )
3		jaod.2	. . 3 |- ( ph -> ( th -> ch ) )
4	2, 3	jaod 729	. 2 |- ( ph -> ( ( ps \/ th ) -> ch ) )
5	1, 4	mpd 13	1 |- ( ph -> ch )

Syntax hints:   -> wi 4   \/ wo 720

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 721

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ifbothdc  3672  opth1  4371  onsucelsucexmidlem  4671  reldmtpos  6514  dftpos4  6524  nnm00  6793  xpfi  7229  omp1eomlem  7424  ctmlemr  7438  ctssdclemn0  7440  finomni  7470  indpi  7699  enq0tr  7791  prarloclem3step  7853  distrlem4prl  7941  distrlem4pru  7942  lelttr  8404  nn1suc  9302  nnsub  9322  nn0lt2  9706  uzin  9934  xrlelttr  10187  xlesubadd  10264  fzfig  10845  seq3id  10940  seq3z  10943  faclbnd  11157  facavg  11162  bcval5  11179  hashfzo  11241  swrdccat3blem  11489  iserex  12083  fsum3cvg  12123  fsumf1o  12135  fisumss  12137  fsumcl2lem  12143  fsumadd  12151  fsummulc2  12193  isumsplit  12236  fprodf1o  12333  prodssdc  12334  fprodssdc  12335  fprodmul  12336  absdvdsb  12554  dvdsabsb  12555  dvdsabseq  12592  m1exp1  12646  flodddiv4  12681  gcdaddm  12739  gcdabs1  12744  lcmdvds  12835  prmind2  12876  rpexp  12909  fermltl  12990  pcxnn0cl  13067  pcxcl  13068  pcabs  13083  pcmpt  13100  pockthg  13114  mulgnn0ass  13938  lgseisenlem2  16104  2lgslem1c  16123  trilpolemcl  16991  trilpolemlt1  16995