Theorem mpjaod 720

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

Syntax hints:   -> wi 4   \/ wo 710

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 711

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ifbothdc  3615  opth1  4299  onsucelsucexmidlem  4596  reldmtpos  6364  dftpos4  6374  nnm00  6641  xpfi  7057  omp1eomlem  7224  ctmlemr  7238  ctssdclemn0  7240  finomni  7270  indpi  7492  enq0tr  7584  prarloclem3step  7646  distrlem4prl  7734  distrlem4pru  7735  lelttr  8198  nn1suc  9092  nnsub  9112  nn0lt2  9491  uzin  9718  xrlelttr  9965  xlesubadd  10042  fzfig  10614  seq3id  10709  seq3z  10712  faclbnd  10925  facavg  10930  bcval5  10947  hashfzo  11006  swrdccat3blem  11232  iserex  11811  fsum3cvg  11850  fsumf1o  11862  fisumss  11864  fsumcl2lem  11870  fsumadd  11878  fsummulc2  11920  isumsplit  11963  fprodf1o  12060  prodssdc  12061  fprodssdc  12062  fprodmul  12063  absdvdsb  12281  dvdsabsb  12282  dvdsabseq  12319  m1exp1  12373  flodddiv4  12408  gcdaddm  12466  gcdabs1  12471  lcmdvds  12562  prmind2  12603  rpexp  12636  fermltl  12717  pcxnn0cl  12794  pcxcl  12795  pcabs  12810  pcmpt  12827  pockthg  12841  mulgnn0ass  13655  lgseisenlem2  15709  2lgslem1c  15728  trilpolemcl  16286  trilpolemlt1  16290