Theorem mpjaod 690

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

Syntax hints:   -> wi 4   \/ wo 680

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ifbothdc  3468  opth1  4116  onsucelsucexmidlem  4402  reldmtpos  6102  dftpos4  6112  nnm00  6377  xpfi  6769  omp1eomlem  6929  ctmlemr  6943  ctssdclemn0  6945  finomni  6960  indpi  7092  enq0tr  7184  prarloclem3step  7246  distrlem4prl  7334  distrlem4pru  7335  lelttr  7769  nn1suc  8643  nnsub  8663  nn0lt2  9030  uzin  9254  xrlelttr  9476  xlesubadd  9553  fzfig  10090  seq3id  10168  seq3z  10171  faclbnd  10374  facavg  10379  bcval5  10396  hashfzo  10455  iserex  10994  fsum3cvg  11032  fsumf1o  11045  fisumss  11047  fsumcl2lem  11053  fsumadd  11061  fsummulc2  11103  isumsplit  11146  absdvdsb  11353  dvdsabsb  11354  dvdsabseq  11387  m1exp1  11440  flodddiv4  11473  gcdaddm  11514  gcdabs1  11519  lcmdvds  11600  prmind2  11641  rpexp  11671  trilpolemcl  12911  trilpolemlt1  12915