Theorem mpjaod 713

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 712	. 2 |- ( ph -> ( ( ps \/ th ) -> ch ) )
5	1, 4	mpd 13	1 |- ( ph -> ch )

Syntax hints:   -> wi 4   \/ wo 703

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 704

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ifbothdc  3558  opth1  4221  onsucelsucexmidlem  4513  reldmtpos  6232  dftpos4  6242  nnm00  6509  xpfi  6907  omp1eomlem  7071  ctmlemr  7085  ctssdclemn0  7087  finomni  7116  indpi  7304  enq0tr  7396  prarloclem3step  7458  distrlem4prl  7546  distrlem4pru  7547  lelttr  8008  nn1suc  8897  nnsub  8917  nn0lt2  9293  uzin  9519  xrlelttr  9763  xlesubadd  9840  fzfig  10386  seq3id  10464  seq3z  10467  faclbnd  10675  facavg  10680  bcval5  10697  hashfzo  10757  iserex  11302  fsum3cvg  11341  fsumf1o  11353  fisumss  11355  fsumcl2lem  11361  fsumadd  11369  fsummulc2  11411  isumsplit  11454  fprodf1o  11551  prodssdc  11552  fprodssdc  11553  fprodmul  11554  absdvdsb  11771  dvdsabsb  11772  dvdsabseq  11807  m1exp1  11860  flodddiv4  11893  gcdaddm  11939  gcdabs1  11944  lcmdvds  12033  prmind2  12074  rpexp  12107  fermltl  12188  pcxnn0cl  12264  pcxcl  12265  pcabs  12279  pcmpt  12295  pockthg  12309  trilpolemcl  14069  trilpolemlt1  14073