Theorem mpjaod 670

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

Syntax hints:   -> wi 4   \/ wo 661

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 662

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  ifbothdc  3380  opth1  3991  onsucelsucexmidlem  4272  reldmtpos  5891  dftpos4  5901  nnm00  6125  indpi  6532  enq0tr  6624  prarloclem3step  6686  distrlem4prl  6774  distrlem4pru  6775  lelttr  7199  nn1suc  8058  nnsub  8077  nn0lt2  8429  uzin  8651  xrlelttr  8876  fzfig  9422  iseqid  9467  iseqz  9469  expival  9478  faclbnd  9668  facavg  9673  ibcval5  9690  iiserex  10177  absdvdsb  10213  dvdsabsb  10214  dvdsabseq  10247  m1exp1  10301  flodddiv4  10334  gcdaddm  10375  gcdabs1  10380  lcmdvds  10461  prmind2  10502  rpexp  10532