Theorem mpjaod 671

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

Syntax hints:   -> wi 4   \/ wo 662

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  ifbothdc  3409  opth1  4037  onsucelsucexmidlem  4318  reldmtpos  5972  dftpos4  5982  nnm00  6240  xpfi  6590  finomni  6740  indpi  6845  enq0tr  6937  prarloclem3step  6999  distrlem4prl  7087  distrlem4pru  7088  lelttr  7517  nn1suc  8376  nnsub  8395  nn0lt2  8761  uzin  8983  xrlelttr  9203  fzfig  9765  iseqid  9843  iseqz  9846  expival  9856  faclbnd  10046  facavg  10051  ibcval5  10068  hashfzo  10127  iiserex  10621  fisumcvg  10658  fsumf1o  10670  fisumss  10672  fsumcl2lem  10677  absdvdsb  10696  dvdsabsb  10697  dvdsabseq  10730  m1exp1  10783  flodddiv4  10816  gcdaddm  10857  gcdabs1  10862  lcmdvds  10943  prmind2  10984  rpexp  11014