Theorem mpjaod 723

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

Syntax hints:   -> wi 4   \/ wo 713

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 714

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ifbothdc  3637  opth1  4321  onsucelsucexmidlem  4620  reldmtpos  6397  dftpos4  6407  nnm00  6674  xpfi  7090  omp1eomlem  7257  ctmlemr  7271  ctssdclemn0  7273  finomni  7303  indpi  7525  enq0tr  7617  prarloclem3step  7679  distrlem4prl  7767  distrlem4pru  7768  lelttr  8231  nn1suc  9125  nnsub  9145  nn0lt2  9524  uzin  9751  xrlelttr  9998  xlesubadd  10075  fzfig  10647  seq3id  10742  seq3z  10745  faclbnd  10958  facavg  10963  bcval5  10980  hashfzo  11039  swrdccat3blem  11266  iserex  11845  fsum3cvg  11884  fsumf1o  11896  fisumss  11898  fsumcl2lem  11904  fsumadd  11912  fsummulc2  11954  isumsplit  11997  fprodf1o  12094  prodssdc  12095  fprodssdc  12096  fprodmul  12097  absdvdsb  12315  dvdsabsb  12316  dvdsabseq  12353  m1exp1  12407  flodddiv4  12442  gcdaddm  12500  gcdabs1  12505  lcmdvds  12596  prmind2  12637  rpexp  12670  fermltl  12751  pcxnn0cl  12828  pcxcl  12829  pcabs  12844  pcmpt  12861  pockthg  12875  mulgnn0ass  13690  lgseisenlem2  15744  2lgslem1c  15763  trilpolemcl  16364  trilpolemlt1  16368