Theorem mpjaod 730

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

This proof depends on syntax axioms:   -> wi 4   \/ wo 720

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721

This proof depends on definitions:  df-bi 117

This theorem is used by:  ifbothdc  3675  opth1  4376  onsucelsucexmidlem  4676  reldmtpos  6524  dftpos4  6534  nnm00  6803  xpfi  7239  omp1eomlem  7434  ctmlemr  7448  ctssdclemn0  7450  finomni  7480  indpi  7709  enq0tr  7801  prarloclem3step  7863  distrlem4prl  7951  distrlem4pru  7952  lelttr  8414  nn1suc  9323  nnsub  9343  nn0lt2  9727  uzin  9955  xrlelttr  10208  xlesubadd  10285  fzfig  10867  seq3id  10962  seq3z  10965  faclbnd  11179  facavg  11184  bcval5  11201  hashfzo  11263  swrdccat3blem  11511  iserex  12105  fsum3cvg  12145  fsumf1o  12157  fisumss  12159  fsumcl2lem  12165  fsumadd  12173  fsummulc2  12215  isumsplit  12258  fprodf1o  12355  prodssdc  12356  fprodssdc  12357  fprodmul  12358  absdvdsb  12576  dvdsabsb  12577  dvdsabseq  12614  m1exp1  12668  flodddiv4  12703  gcdaddm  12761  gcdabs1  12766  lcmdvds  12857  prmind2  12898  rpexp  12931  fermltl  13012  pcxnn0cl  13089  pcxcl  13090  pcabs  13105  pcmpt  13122  pockthg  13136  mulgnn0ass  13961  lgseisenlem2  16190  2lgslem1c  16209  trilpolemcl  17086  trilpolemlt1  17090