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  3591  opth1  4266  onsucelsucexmidlem  4562  reldmtpos  6308  dftpos4  6318  nnm00  6585  xpfi  6988  omp1eomlem  7155  ctmlemr  7169  ctssdclemn0  7171  finomni  7201  indpi  7404  enq0tr  7496  prarloclem3step  7558  distrlem4prl  7646  distrlem4pru  7647  lelttr  8110  nn1suc  9003  nnsub  9023  nn0lt2  9401  uzin  9628  xrlelttr  9875  xlesubadd  9952  fzfig  10504  seq3id  10599  seq3z  10602  faclbnd  10815  facavg  10820  bcval5  10837  hashfzo  10896  iserex  11485  fsum3cvg  11524  fsumf1o  11536  fisumss  11538  fsumcl2lem  11544  fsumadd  11552  fsummulc2  11594  isumsplit  11637  fprodf1o  11734  prodssdc  11735  fprodssdc  11736  fprodmul  11737  absdvdsb  11955  dvdsabsb  11956  dvdsabseq  11992  m1exp1  12045  flodddiv4  12078  gcdaddm  12124  gcdabs1  12129  lcmdvds  12220  prmind2  12261  rpexp  12294  fermltl  12375  pcxnn0cl  12451  pcxcl  12452  pcabs  12467  pcmpt  12484  pockthg  12498  mulgnn0ass  13231  lgseisenlem2  15228  2lgslem1c  15247  trilpolemcl  15597  trilpolemlt1  15601