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  3568  opth1  4237  onsucelsucexmidlem  4529  reldmtpos  6254  dftpos4  6264  nnm00  6531  xpfi  6929  omp1eomlem  7093  ctmlemr  7107  ctssdclemn0  7109  finomni  7138  indpi  7341  enq0tr  7433  prarloclem3step  7495  distrlem4prl  7583  distrlem4pru  7584  lelttr  8046  nn1suc  8938  nnsub  8958  nn0lt2  9334  uzin  9560  xrlelttr  9806  xlesubadd  9883  fzfig  10430  seq3id  10508  seq3z  10511  faclbnd  10721  facavg  10726  bcval5  10743  hashfzo  10802  iserex  11347  fsum3cvg  11386  fsumf1o  11398  fisumss  11400  fsumcl2lem  11406  fsumadd  11414  fsummulc2  11456  isumsplit  11499  fprodf1o  11596  prodssdc  11597  fprodssdc  11598  fprodmul  11599  absdvdsb  11816  dvdsabsb  11817  dvdsabseq  11853  m1exp1  11906  flodddiv4  11939  gcdaddm  11985  gcdabs1  11990  lcmdvds  12079  prmind2  12120  rpexp  12153  fermltl  12234  pcxnn0cl  12310  pcxcl  12311  pcabs  12325  pcmpt  12341  pockthg  12355  mulgnn0ass  13019  lgseisenlem2  14454  trilpolemcl  14788  trilpolemlt1  14792