Theorem mpjaod 723

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

Syntax hints:   -> wi 4   \/ wo 713

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 714

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ifbothdc  3637  opth1  4322  onsucelsucexmidlem  4621  reldmtpos  6405  dftpos4  6415  nnm00  6684  xpfi  7105  omp1eomlem  7272  ctmlemr  7286  ctssdclemn0  7288  finomni  7318  indpi  7540  enq0tr  7632  prarloclem3step  7694  distrlem4prl  7782  distrlem4pru  7783  lelttr  8246  nn1suc  9140  nnsub  9160  nn0lt2  9539  uzin  9767  xrlelttr  10014  xlesubadd  10091  fzfig  10664  seq3id  10759  seq3z  10762  faclbnd  10975  facavg  10980  bcval5  10997  hashfzo  11057  swrdccat3blem  11286  iserex  11865  fsum3cvg  11904  fsumf1o  11916  fisumss  11918  fsumcl2lem  11924  fsumadd  11932  fsummulc2  11974  isumsplit  12017  fprodf1o  12114  prodssdc  12115  fprodssdc  12116  fprodmul  12117  absdvdsb  12335  dvdsabsb  12336  dvdsabseq  12373  m1exp1  12427  flodddiv4  12462  gcdaddm  12520  gcdabs1  12525  lcmdvds  12616  prmind2  12657  rpexp  12690  fermltl  12771  pcxnn0cl  12848  pcxcl  12849  pcabs  12864  pcmpt  12881  pockthg  12895  mulgnn0ass  13710  lgseisenlem2  15765  2lgslem1c  15784  trilpolemcl  16465  trilpolemlt1  16469