Theorem mpjaod 708

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

Syntax hints:   -> wi 4   \/ wo 698

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ifbothdc  3552  opth1  4214  onsucelsucexmidlem  4506  reldmtpos  6221  dftpos4  6231  nnm00  6497  xpfi  6895  omp1eomlem  7059  ctmlemr  7073  ctssdclemn0  7075  finomni  7104  indpi  7283  enq0tr  7375  prarloclem3step  7437  distrlem4prl  7525  distrlem4pru  7526  lelttr  7987  nn1suc  8876  nnsub  8896  nn0lt2  9272  uzin  9498  xrlelttr  9742  xlesubadd  9819  fzfig  10365  seq3id  10443  seq3z  10446  faclbnd  10654  facavg  10659  bcval5  10676  hashfzo  10735  iserex  11280  fsum3cvg  11319  fsumf1o  11331  fisumss  11333  fsumcl2lem  11339  fsumadd  11347  fsummulc2  11389  isumsplit  11432  fprodf1o  11529  prodssdc  11530  fprodssdc  11531  fprodmul  11532  absdvdsb  11749  dvdsabsb  11750  dvdsabseq  11785  m1exp1  11838  flodddiv4  11871  gcdaddm  11917  gcdabs1  11922  lcmdvds  12011  prmind2  12052  rpexp  12085  fermltl  12166  pcxnn0cl  12242  pcxcl  12243  pcabs  12257  pcmpt  12273  pockthg  12287  trilpolemcl  13916  trilpolemlt1  13920