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  3638  opth1  4326  onsucelsucexmidlem  4625  reldmtpos  6414  dftpos4  6424  nnm00  6693  xpfi  7117  omp1eomlem  7284  ctmlemr  7298  ctssdclemn0  7300  finomni  7330  indpi  7552  enq0tr  7644  prarloclem3step  7706  distrlem4prl  7794  distrlem4pru  7795  lelttr  8258  nn1suc  9152  nnsub  9172  nn0lt2  9551  uzin  9779  xrlelttr  10031  xlesubadd  10108  fzfig  10682  seq3id  10777  seq3z  10780  faclbnd  10993  facavg  10998  bcval5  11015  hashfzo  11076  swrdccat3blem  11310  iserex  11890  fsum3cvg  11929  fsumf1o  11941  fisumss  11943  fsumcl2lem  11949  fsumadd  11957  fsummulc2  11999  isumsplit  12042  fprodf1o  12139  prodssdc  12140  fprodssdc  12141  fprodmul  12142  absdvdsb  12360  dvdsabsb  12361  dvdsabseq  12398  m1exp1  12452  flodddiv4  12487  gcdaddm  12545  gcdabs1  12550  lcmdvds  12641  prmind2  12682  rpexp  12715  fermltl  12796  pcxnn0cl  12873  pcxcl  12874  pcabs  12889  pcmpt  12906  pockthg  12920  mulgnn0ass  13735  lgseisenlem2  15790  2lgslem1c  15809  trilpolemcl  16577  trilpolemlt1  16581