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  3604  opth1  4279  onsucelsucexmidlem  4575  reldmtpos  6329  dftpos4  6339  nnm00  6606  xpfi  7011  omp1eomlem  7178  ctmlemr  7192  ctssdclemn0  7194  finomni  7224  indpi  7437  enq0tr  7529  prarloclem3step  7591  distrlem4prl  7679  distrlem4pru  7680  lelttr  8143  nn1suc  9037  nnsub  9057  nn0lt2  9436  uzin  9663  xrlelttr  9910  xlesubadd  9987  fzfig  10556  seq3id  10651  seq3z  10654  faclbnd  10867  facavg  10872  bcval5  10889  hashfzo  10948  iserex  11569  fsum3cvg  11608  fsumf1o  11620  fisumss  11622  fsumcl2lem  11628  fsumadd  11636  fsummulc2  11678  isumsplit  11721  fprodf1o  11818  prodssdc  11819  fprodssdc  11820  fprodmul  11821  absdvdsb  12039  dvdsabsb  12040  dvdsabseq  12077  m1exp1  12131  flodddiv4  12166  gcdaddm  12224  gcdabs1  12229  lcmdvds  12320  prmind2  12361  rpexp  12394  fermltl  12475  pcxnn0cl  12552  pcxcl  12553  pcabs  12568  pcmpt  12585  pockthg  12599  mulgnn0ass  13412  lgseisenlem2  15466  2lgslem1c  15485  trilpolemcl  15840  trilpolemlt1  15844