Theorem mpjaod 726

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

Syntax hints:   -> wi 4   \/ wo 716

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 717

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ifbothdc  3644  opth1  4334  onsucelsucexmidlem  4633  reldmtpos  6462  dftpos4  6472  nnm00  6741  xpfi  7167  omp1eomlem  7336  ctmlemr  7350  ctssdclemn0  7352  finomni  7382  indpi  7605  enq0tr  7697  prarloclem3step  7759  distrlem4prl  7847  distrlem4pru  7848  lelttr  8310  nn1suc  9204  nnsub  9224  nn0lt2  9605  uzin  9833  xrlelttr  10085  xlesubadd  10162  fzfig  10738  seq3id  10833  seq3z  10836  faclbnd  11049  facavg  11054  bcval5  11071  hashfzo  11132  swrdccat3blem  11369  iserex  11962  fsum3cvg  12002  fsumf1o  12014  fisumss  12016  fsumcl2lem  12022  fsumadd  12030  fsummulc2  12072  isumsplit  12115  fprodf1o  12212  prodssdc  12213  fprodssdc  12214  fprodmul  12215  absdvdsb  12433  dvdsabsb  12434  dvdsabseq  12471  m1exp1  12525  flodddiv4  12560  gcdaddm  12618  gcdabs1  12623  lcmdvds  12714  prmind2  12755  rpexp  12788  fermltl  12869  pcxnn0cl  12946  pcxcl  12947  pcabs  12962  pcmpt  12979  pockthg  12993  mulgnn0ass  13808  lgseisenlem2  15873  2lgslem1c  15892  trilpolemcl  16752  trilpolemlt1  16756