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  3657  opth1  4352  onsucelsucexmidlem  4651  reldmtpos  6484  dftpos4  6494  nnm00  6763  xpfi  7192  omp1eomlem  7385  ctmlemr  7399  ctssdclemn0  7401  finomni  7431  indpi  7657  enq0tr  7749  prarloclem3step  7811  distrlem4prl  7899  distrlem4pru  7900  lelttr  8362  nn1suc  9256  nnsub  9276  nn0lt2  9659  uzin  9887  xrlelttr  10139  xlesubadd  10216  fzfig  10792  seq3id  10887  seq3z  10890  faclbnd  11103  facavg  11108  bcval5  11125  hashfzo  11187  swrdccat3blem  11431  iserex  12024  fsum3cvg  12064  fsumf1o  12076  fisumss  12078  fsumcl2lem  12084  fsumadd  12092  fsummulc2  12134  isumsplit  12177  fprodf1o  12274  prodssdc  12275  fprodssdc  12276  fprodmul  12277  absdvdsb  12495  dvdsabsb  12496  dvdsabseq  12533  m1exp1  12587  flodddiv4  12622  gcdaddm  12680  gcdabs1  12685  lcmdvds  12776  prmind2  12817  rpexp  12850  fermltl  12931  pcxnn0cl  13008  pcxcl  13009  pcabs  13024  pcmpt  13041  pockthg  13055  mulgnn0ass  13875  lgseisenlem2  15944  2lgslem1c  15963  trilpolemcl  16821  trilpolemlt1  16825