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  3604  opth1  4279  onsucelsucexmidlem  4576  reldmtpos  6338  dftpos4  6348  nnm00  6615  xpfi  7028  omp1eomlem  7195  ctmlemr  7209  ctssdclemn0  7211  finomni  7241  indpi  7454  enq0tr  7546  prarloclem3step  7608  distrlem4prl  7696  distrlem4pru  7697  lelttr  8160  nn1suc  9054  nnsub  9074  nn0lt2  9453  uzin  9680  xrlelttr  9927  xlesubadd  10004  fzfig  10573  seq3id  10668  seq3z  10671  faclbnd  10884  facavg  10889  bcval5  10906  hashfzo  10965  iserex  11621  fsum3cvg  11660  fsumf1o  11672  fisumss  11674  fsumcl2lem  11680  fsumadd  11688  fsummulc2  11730  isumsplit  11773  fprodf1o  11870  prodssdc  11871  fprodssdc  11872  fprodmul  11873  absdvdsb  12091  dvdsabsb  12092  dvdsabseq  12129  m1exp1  12183  flodddiv4  12218  gcdaddm  12276  gcdabs1  12281  lcmdvds  12372  prmind2  12413  rpexp  12446  fermltl  12527  pcxnn0cl  12604  pcxcl  12605  pcabs  12620  pcmpt  12637  pockthg  12651  mulgnn0ass  13465  lgseisenlem2  15519  2lgslem1c  15538  trilpolemcl  15938  trilpolemlt1  15942