Theorem mpjaod 725

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

Syntax hints:   -> wi 4   \/ wo 715

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 716

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ifbothdc  3640  opth1  4328  onsucelsucexmidlem  4627  reldmtpos  6419  dftpos4  6429  nnm00  6698  xpfi  7124  omp1eomlem  7293  ctmlemr  7307  ctssdclemn0  7309  finomni  7339  indpi  7562  enq0tr  7654  prarloclem3step  7716  distrlem4prl  7804  distrlem4pru  7805  lelttr  8268  nn1suc  9162  nnsub  9182  nn0lt2  9561  uzin  9789  xrlelttr  10041  xlesubadd  10118  fzfig  10693  seq3id  10788  seq3z  10791  faclbnd  11004  facavg  11009  bcval5  11026  hashfzo  11087  swrdccat3blem  11324  iserex  11917  fsum3cvg  11957  fsumf1o  11969  fisumss  11971  fsumcl2lem  11977  fsumadd  11985  fsummulc2  12027  isumsplit  12070  fprodf1o  12167  prodssdc  12168  fprodssdc  12169  fprodmul  12170  absdvdsb  12388  dvdsabsb  12389  dvdsabseq  12426  m1exp1  12480  flodddiv4  12515  gcdaddm  12573  gcdabs1  12578  lcmdvds  12669  prmind2  12710  rpexp  12743  fermltl  12824  pcxnn0cl  12901  pcxcl  12902  pcabs  12917  pcmpt  12934  pockthg  12948  mulgnn0ass  13763  lgseisenlem2  15819  2lgslem1c  15838  trilpolemcl  16692  trilpolemlt1  16696