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  3594  opth1  4269  onsucelsucexmidlem  4565  reldmtpos  6311  dftpos4  6321  nnm00  6588  xpfi  6993  omp1eomlem  7160  ctmlemr  7174  ctssdclemn0  7176  finomni  7206  indpi  7409  enq0tr  7501  prarloclem3step  7563  distrlem4prl  7651  distrlem4pru  7652  lelttr  8115  nn1suc  9009  nnsub  9029  nn0lt2  9407  uzin  9634  xrlelttr  9881  xlesubadd  9958  fzfig  10522  seq3id  10617  seq3z  10620  faclbnd  10833  facavg  10838  bcval5  10855  hashfzo  10914  iserex  11504  fsum3cvg  11543  fsumf1o  11555  fisumss  11557  fsumcl2lem  11563  fsumadd  11571  fsummulc2  11613  isumsplit  11656  fprodf1o  11753  prodssdc  11754  fprodssdc  11755  fprodmul  11756  absdvdsb  11974  dvdsabsb  11975  dvdsabseq  12012  m1exp1  12066  flodddiv4  12101  gcdaddm  12151  gcdabs1  12156  lcmdvds  12247  prmind2  12288  rpexp  12321  fermltl  12402  pcxnn0cl  12479  pcxcl  12480  pcabs  12495  pcmpt  12512  pockthg  12526  mulgnn0ass  13288  lgseisenlem2  15312  2lgslem1c  15331  trilpolemcl  15681  trilpolemlt1  15685