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  3567  opth1  4236  onsucelsucexmidlem  4528  reldmtpos  6253  dftpos4  6263  nnm00  6530  xpfi  6928  omp1eomlem  7092  ctmlemr  7106  ctssdclemn0  7108  finomni  7137  indpi  7340  enq0tr  7432  prarloclem3step  7494  distrlem4prl  7582  distrlem4pru  7583  lelttr  8045  nn1suc  8937  nnsub  8957  nn0lt2  9333  uzin  9559  xrlelttr  9805  xlesubadd  9882  fzfig  10429  seq3id  10507  seq3z  10510  faclbnd  10720  facavg  10725  bcval5  10742  hashfzo  10801  iserex  11346  fsum3cvg  11385  fsumf1o  11397  fisumss  11399  fsumcl2lem  11405  fsumadd  11413  fsummulc2  11455  isumsplit  11498  fprodf1o  11595  prodssdc  11596  fprodssdc  11597  fprodmul  11598  absdvdsb  11815  dvdsabsb  11816  dvdsabseq  11852  m1exp1  11905  flodddiv4  11938  gcdaddm  11984  gcdabs1  11989  lcmdvds  12078  prmind2  12119  rpexp  12152  fermltl  12233  pcxnn0cl  12309  pcxcl  12310  pcabs  12324  pcmpt  12340  pockthg  12354  mulgnn0ass  13017  lgseisenlem2  14421  trilpolemcl  14755  trilpolemlt1  14759