Theorem mpjaod 730

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

This proof depends on syntax axioms:   -> wi 4   \/ wo 720

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721

This proof depends on definitions:  df-bi 117

This theorem is used by:  ifbothdc  3675  opth1  4378  onsucelsucexmidlem  4678  reldmtpos  6528  dftpos4  6538  nnm00  6807  xpfi  7243  omp1eomlem  7440  ctmlemr  7454  ctssdclemn0  7456  finomni  7486  indpi  7715  enq0tr  7807  prarloclem3step  7869  distrlem4prl  7957  distrlem4pru  7958  lelttr  8420  nn1suc  9332  nnsub  9352  nn0lt2  9738  uzin  9971  xrlelttr  10225  xlesubadd  10302  fzfig  10888  seq3id  10983  seq3z  10986  faclbnd  11201  facavg  11206  bcval5  11223  hashfzo  11285  swrdccat3blem  11533  iserex  12130  fsum3cvg  12170  fsumf1o  12182  fisumss  12184  fsumcl2lem  12190  fsumadd  12198  fsummulc2  12240  isumsplit  12283  fprodf1o  12380  prodssdc  12381  fprodssdc  12382  fprodmul  12383  absdvdsb  12601  dvdsabsb  12602  dvdsabseq  12639  m1exp1  12693  flodddiv4  12728  gcdaddm  12786  gcdabs1  12791  lcmdvds  12882  prmind2  12923  rpexp  12957  fermltl  13041  pcxnn0cl  13118  pcxcl  13119  pcabs  13134  pcmpt  13151  pockthg  13165  prmlem0  13249  prmlem1a  13250  mulgnn0ass  14020  chtublem  16295  bpos1lem  16309  bposlem1  16311  bposlem3  16313  lgseisenlem2  16395  2lgslem1c  16414  trilpolemcl  17293  trilpolemlt1  17297