Theorem mpjaod 719

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

Syntax hints:   -> wi 4   \/ wo 709

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 710

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ifbothdc  3582  opth1  4254  onsucelsucexmidlem  4546  reldmtpos  6277  dftpos4  6287  nnm00  6554  xpfi  6957  omp1eomlem  7122  ctmlemr  7136  ctssdclemn0  7138  finomni  7167  indpi  7370  enq0tr  7462  prarloclem3step  7524  distrlem4prl  7612  distrlem4pru  7613  lelttr  8075  nn1suc  8967  nnsub  8987  nn0lt2  9363  uzin  9589  xrlelttr  9835  xlesubadd  9912  fzfig  10460  seq3id  10538  seq3z  10541  faclbnd  10752  facavg  10757  bcval5  10774  hashfzo  10833  iserex  11378  fsum3cvg  11417  fsumf1o  11429  fisumss  11431  fsumcl2lem  11437  fsumadd  11445  fsummulc2  11487  isumsplit  11530  fprodf1o  11627  prodssdc  11628  fprodssdc  11629  fprodmul  11630  absdvdsb  11847  dvdsabsb  11848  dvdsabseq  11884  m1exp1  11937  flodddiv4  11970  gcdaddm  12016  gcdabs1  12021  lcmdvds  12110  prmind2  12151  rpexp  12184  fermltl  12265  pcxnn0cl  12341  pcxcl  12342  pcabs  12357  pcmpt  12374  pockthg  12388  mulgnn0ass  13095  lgseisenlem2  14904  trilpolemcl  15239  trilpolemlt1  15243