Theorem mpjaod 718

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

Syntax hints:   -> wi 4   \/ wo 708

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 709

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ifbothdc  3564  opth1  4230  onsucelsucexmidlem  4522  reldmtpos  6244  dftpos4  6254  nnm00  6521  xpfi  6919  omp1eomlem  7083  ctmlemr  7097  ctssdclemn0  7099  finomni  7128  indpi  7316  enq0tr  7408  prarloclem3step  7470  distrlem4prl  7558  distrlem4pru  7559  lelttr  8020  nn1suc  8911  nnsub  8931  nn0lt2  9307  uzin  9533  xrlelttr  9777  xlesubadd  9854  fzfig  10400  seq3id  10478  seq3z  10481  faclbnd  10689  facavg  10694  bcval5  10711  hashfzo  10770  iserex  11315  fsum3cvg  11354  fsumf1o  11366  fisumss  11368  fsumcl2lem  11374  fsumadd  11382  fsummulc2  11424  isumsplit  11467  fprodf1o  11564  prodssdc  11565  fprodssdc  11566  fprodmul  11567  absdvdsb  11784  dvdsabsb  11785  dvdsabseq  11820  m1exp1  11873  flodddiv4  11906  gcdaddm  11952  gcdabs1  11957  lcmdvds  12046  prmind2  12087  rpexp  12120  fermltl  12201  pcxnn0cl  12277  pcxcl  12278  pcabs  12292  pcmpt  12308  pockthg  12322  mulgnn0ass  12879  trilpolemcl  14346  trilpolemlt1  14350