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  4376  onsucelsucexmidlem  4676  reldmtpos  6524  dftpos4  6534  nnm00  6803  xpfi  7239  omp1eomlem  7434  ctmlemr  7448  ctssdclemn0  7450  finomni  7480  indpi  7709  enq0tr  7801  prarloclem3step  7863  distrlem4prl  7951  distrlem4pru  7952  lelttr  8414  nn1suc  9325  nnsub  9345  nn0lt2  9731  uzin  9964  xrlelttr  10218  xlesubadd  10295  fzfig  10880  seq3id  10975  seq3z  10978  faclbnd  11193  facavg  11198  bcval5  11215  hashfzo  11277  swrdccat3blem  11525  iserex  12121  fsum3cvg  12161  fsumf1o  12173  fisumss  12175  fsumcl2lem  12181  fsumadd  12189  fsummulc2  12231  isumsplit  12274  fprodf1o  12371  prodssdc  12372  fprodssdc  12373  fprodmul  12374  absdvdsb  12592  dvdsabsb  12593  dvdsabseq  12630  m1exp1  12684  flodddiv4  12719  gcdaddm  12777  gcdabs1  12782  lcmdvds  12873  prmind2  12914  rpexp  12948  fermltl  13032  pcxnn0cl  13109  pcxcl  13110  pcabs  13125  pcmpt  13142  pockthg  13156  prmlem0  13240  prmlem1a  13241  mulgnn0ass  14010  bpos1lem  16207  bposlem1  16209  bposlem3  16211  lgseisenlem2  16288  2lgslem1c  16307  trilpolemcl  17184  trilpolemlt1  17188