Theorem mpjaod 719

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

Syntax hints:   -> wi 4   \/ wo 709

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 710

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ifbothdc  3595  opth1  4270  onsucelsucexmidlem  4566  reldmtpos  6320  dftpos4  6330  nnm00  6597  xpfi  7002  omp1eomlem  7169  ctmlemr  7183  ctssdclemn0  7185  finomni  7215  indpi  7426  enq0tr  7518  prarloclem3step  7580  distrlem4prl  7668  distrlem4pru  7669  lelttr  8132  nn1suc  9026  nnsub  9046  nn0lt2  9424  uzin  9651  xrlelttr  9898  xlesubadd  9975  fzfig  10539  seq3id  10634  seq3z  10637  faclbnd  10850  facavg  10855  bcval5  10872  hashfzo  10931  iserex  11521  fsum3cvg  11560  fsumf1o  11572  fisumss  11574  fsumcl2lem  11580  fsumadd  11588  fsummulc2  11630  isumsplit  11673  fprodf1o  11770  prodssdc  11771  fprodssdc  11772  fprodmul  11773  absdvdsb  11991  dvdsabsb  11992  dvdsabseq  12029  m1exp1  12083  flodddiv4  12118  gcdaddm  12176  gcdabs1  12181  lcmdvds  12272  prmind2  12313  rpexp  12346  fermltl  12427  pcxnn0cl  12504  pcxcl  12505  pcabs  12520  pcmpt  12537  pockthg  12551  mulgnn0ass  13364  lgseisenlem2  15396  2lgslem1c  15415  trilpolemcl  15768  trilpolemlt1  15772