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  7435  ctmlemr  7449  ctssdclemn0  7451  finomni  7481  indpi  7710  enq0tr  7802  prarloclem3step  7864  distrlem4prl  7952  distrlem4pru  7953  lelttr  8415  nn1suc  9326  nnsub  9346  nn0lt2  9732  uzin  9965  xrlelttr  10219  xlesubadd  10296  fzfig  10882  seq3id  10977  seq3z  10980  faclbnd  11195  facavg  11200  bcval5  11217  hashfzo  11279  swrdccat3blem  11527  iserex  12124  fsum3cvg  12164  fsumf1o  12176  fisumss  12178  fsumcl2lem  12184  fsumadd  12192  fsummulc2  12234  isumsplit  12277  fprodf1o  12374  prodssdc  12375  fprodssdc  12376  fprodmul  12377  absdvdsb  12595  dvdsabsb  12596  dvdsabseq  12633  m1exp1  12687  flodddiv4  12722  gcdaddm  12780  gcdabs1  12785  lcmdvds  12876  prmind2  12917  rpexp  12951  fermltl  13035  pcxnn0cl  13112  pcxcl  13113  pcabs  13128  pcmpt  13145  pockthg  13159  prmlem0  13243  prmlem1a  13244  mulgnn0ass  14014  chtublem  16256  bpos1lem  16270  bposlem1  16272  bposlem3  16274  lgseisenlem2  16356  2lgslem1c  16375  trilpolemcl  17253  trilpolemlt1  17257