Theorem mpjaod 725

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

Syntax hints:   -> wi 4   \/ wo 715

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 716

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ifbothdc  3640  opth1  4328  onsucelsucexmidlem  4627  reldmtpos  6418  dftpos4  6428  nnm00  6697  xpfi  7123  omp1eomlem  7292  ctmlemr  7306  ctssdclemn0  7308  finomni  7338  indpi  7561  enq0tr  7653  prarloclem3step  7715  distrlem4prl  7803  distrlem4pru  7804  lelttr  8267  nn1suc  9161  nnsub  9181  nn0lt2  9560  uzin  9788  xrlelttr  10040  xlesubadd  10117  fzfig  10691  seq3id  10786  seq3z  10789  faclbnd  11002  facavg  11007  bcval5  11024  hashfzo  11085  swrdccat3blem  11319  iserex  11899  fsum3cvg  11938  fsumf1o  11950  fisumss  11952  fsumcl2lem  11958  fsumadd  11966  fsummulc2  12008  isumsplit  12051  fprodf1o  12148  prodssdc  12149  fprodssdc  12150  fprodmul  12151  absdvdsb  12369  dvdsabsb  12370  dvdsabseq  12407  m1exp1  12461  flodddiv4  12496  gcdaddm  12554  gcdabs1  12559  lcmdvds  12650  prmind2  12691  rpexp  12724  fermltl  12805  pcxnn0cl  12882  pcxcl  12883  pcabs  12898  pcmpt  12915  pockthg  12929  mulgnn0ass  13744  lgseisenlem2  15799  2lgslem1c  15818  trilpolemcl  16641  trilpolemlt1  16645