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  11592  fsum3cvg  11631  fsumf1o  11643  fisumss  11645  fsumcl2lem  11651  fsumadd  11659  fsummulc2  11701  isumsplit  11744  fprodf1o  11841  prodssdc  11842  fprodssdc  11843  fprodmul  11844  absdvdsb  12062  dvdsabsb  12063  dvdsabseq  12100  m1exp1  12154  flodddiv4  12189  gcdaddm  12247  gcdabs1  12252  lcmdvds  12343  prmind2  12384  rpexp  12417  fermltl  12498  pcxnn0cl  12575  pcxcl  12576  pcabs  12591  pcmpt  12608  pockthg  12622  mulgnn0ass  13436  lgseisenlem2  15490  2lgslem1c  15509  trilpolemcl  15909  trilpolemlt1  15913