Theorem mpjaod 720

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 719	. 2 |- ( ph -> ( ( ps \/ th ) -> ch ) )
5	1, 4	mpd 13	1 |- ( ph -> ch )

Syntax hints:   -> wi 4   \/ wo 710

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 711

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ifbothdc  3610  opth1  4288  onsucelsucexmidlem  4585  reldmtpos  6352  dftpos4  6362  nnm00  6629  xpfi  7044  omp1eomlem  7211  ctmlemr  7225  ctssdclemn0  7227  finomni  7257  indpi  7475  enq0tr  7567  prarloclem3step  7629  distrlem4prl  7717  distrlem4pru  7718  lelttr  8181  nn1suc  9075  nnsub  9095  nn0lt2  9474  uzin  9701  xrlelttr  9948  xlesubadd  10025  fzfig  10597  seq3id  10692  seq3z  10695  faclbnd  10908  facavg  10913  bcval5  10930  hashfzo  10989  iserex  11725  fsum3cvg  11764  fsumf1o  11776  fisumss  11778  fsumcl2lem  11784  fsumadd  11792  fsummulc2  11834  isumsplit  11877  fprodf1o  11974  prodssdc  11975  fprodssdc  11976  fprodmul  11977  absdvdsb  12195  dvdsabsb  12196  dvdsabseq  12233  m1exp1  12287  flodddiv4  12322  gcdaddm  12380  gcdabs1  12385  lcmdvds  12476  prmind2  12517  rpexp  12550  fermltl  12631  pcxnn0cl  12708  pcxcl  12709  pcabs  12724  pcmpt  12741  pockthg  12755  mulgnn0ass  13569  lgseisenlem2  15623  2lgslem1c  15642  trilpolemcl  16117  trilpolemlt1  16121