Theorem mpjaod 726

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

Syntax hints:   -> wi 4   \/ wo 716

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 717

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ifbothdc  3662  opth1  4358  onsucelsucexmidlem  4658  reldmtpos  6499  dftpos4  6509  nnm00  6778  xpfi  7207  omp1eomlem  7400  ctmlemr  7414  ctssdclemn0  7416  finomni  7446  indpi  7675  enq0tr  7767  prarloclem3step  7829  distrlem4prl  7917  distrlem4pru  7918  lelttr  8380  nn1suc  9278  nnsub  9298  nn0lt2  9682  uzin  9910  xrlelttr  10163  xlesubadd  10240  fzfig  10821  seq3id  10916  seq3z  10919  faclbnd  11133  facavg  11138  bcval5  11155  hashfzo  11217  swrdccat3blem  11461  iserex  12055  fsum3cvg  12095  fsumf1o  12107  fisumss  12109  fsumcl2lem  12115  fsumadd  12123  fsummulc2  12165  isumsplit  12208  fprodf1o  12305  prodssdc  12306  fprodssdc  12307  fprodmul  12308  absdvdsb  12526  dvdsabsb  12527  dvdsabseq  12564  m1exp1  12618  flodddiv4  12653  gcdaddm  12711  gcdabs1  12716  lcmdvds  12807  prmind2  12848  rpexp  12881  fermltl  12962  pcxnn0cl  13039  pcxcl  13040  pcabs  13055  pcmpt  13072  pockthg  13086  mulgnn0ass  13917  lgseisenlem2  16076  2lgslem1c  16095  trilpolemcl  16963  trilpolemlt1  16967