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  3590  opth1  4265  onsucelsucexmidlem  4561  reldmtpos  6306  dftpos4  6316  nnm00  6583  xpfi  6986  omp1eomlem  7153  ctmlemr  7167  ctssdclemn0  7169  finomni  7199  indpi  7402  enq0tr  7494  prarloclem3step  7556  distrlem4prl  7644  distrlem4pru  7645  lelttr  8108  nn1suc  9001  nnsub  9021  nn0lt2  9398  uzin  9625  xrlelttr  9872  xlesubadd  9949  fzfig  10501  seq3id  10596  seq3z  10599  faclbnd  10812  facavg  10817  bcval5  10834  hashfzo  10893  iserex  11482  fsum3cvg  11521  fsumf1o  11533  fisumss  11535  fsumcl2lem  11541  fsumadd  11549  fsummulc2  11591  isumsplit  11634  fprodf1o  11731  prodssdc  11732  fprodssdc  11733  fprodmul  11734  absdvdsb  11952  dvdsabsb  11953  dvdsabseq  11989  m1exp1  12042  flodddiv4  12075  gcdaddm  12121  gcdabs1  12126  lcmdvds  12217  prmind2  12258  rpexp  12291  fermltl  12372  pcxnn0cl  12448  pcxcl  12449  pcabs  12464  pcmpt  12481  pockthg  12495  mulgnn0ass  13228  lgseisenlem2  15187  trilpolemcl  15527  trilpolemlt1  15531