Theorem mpjaod 726

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

Syntax hints:   -> wi 4   \/ wo 716

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 717

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ifbothdc  3661  opth1  4357  onsucelsucexmidlem  4656  reldmtpos  6497  dftpos4  6507  nnm00  6776  xpfi  7205  omp1eomlem  7398  ctmlemr  7412  ctssdclemn0  7414  finomni  7444  indpi  7673  enq0tr  7765  prarloclem3step  7827  distrlem4prl  7915  distrlem4pru  7916  lelttr  8378  nn1suc  9273  nnsub  9293  nn0lt2  9677  uzin  9905  xrlelttr  10158  xlesubadd  10235  fzfig  10816  seq3id  10911  seq3z  10914  faclbnd  11128  facavg  11133  bcval5  11150  hashfzo  11212  swrdccat3blem  11456  iserex  12049  fsum3cvg  12089  fsumf1o  12101  fisumss  12103  fsumcl2lem  12109  fsumadd  12117  fsummulc2  12159  isumsplit  12202  fprodf1o  12299  prodssdc  12300  fprodssdc  12301  fprodmul  12302  absdvdsb  12520  dvdsabsb  12521  dvdsabseq  12558  m1exp1  12612  flodddiv4  12647  gcdaddm  12705  gcdabs1  12710  lcmdvds  12801  prmind2  12842  rpexp  12875  fermltl  12956  pcxnn0cl  13033  pcxcl  13034  pcabs  13049  pcmpt  13066  pockthg  13080  mulgnn0ass  13911  lgseisenlem2  16070  2lgslem1c  16089  trilpolemcl  16947  trilpolemlt1  16951