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  6529  dftpos4  6539  nnm00  6808  xpfi  7245  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  9736  uzin  9970  xrlelttr  10224  xlesubadd  10301  fzfig  10887  seq3id  10982  seq3z  10985  faclbnd  11200  facavg  11205  bcval5  11222  hashfzo  11284  swrdccat3blem  11532  iserex  12129  fsum3cvg  12169  fsumf1o  12181  fisumss  12183  fsumcl2lem  12189  fsumadd  12197  fsummulc2  12239  isumsplit  12282  fprodf1o  12379  prodssdc  12380  fprodssdc  12381  fprodmul  12382  absdvdsb  12600  dvdsabsb  12601  dvdsabseq  12638  m1exp1  12692  flodddiv4  12727  gcdaddm  12785  gcdabs1  12790  lcmdvds  12881  prmind2  12922  rpexp  12956  fermltl  13040  pcxnn0cl  13117  pcxcl  13118  pcabs  13133  pcmpt  13150  pockthg  13164  prmlem0  13248  prmlem1a  13249  mulgnn0ass  14019  chtublem  16312  bpos1lem  16326  bposlem1  16328  bposlem3  16330  lgseisenlem2  16412  2lgslem1c  16431  trilpolemcl  17310  trilpolemlt1  17314