ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mpjaod Unicode version

Theorem mpjaod 671
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
StepHypRef Expression
1 jaod.3 . 2  |-  ( ph  ->  ( ps  \/  th ) )
2 jaod.1 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
3 jaod.2 . . 3  |-  ( ph  ->  ( th  ->  ch ) )
42, 3jaod 670 . 2  |-  ( ph  ->  ( ( ps  \/  th )  ->  ch )
)
51, 4mpd 13 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 662
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  ifbothdc  3409  opth1  4037  onsucelsucexmidlem  4318  reldmtpos  5972  dftpos4  5982  nnm00  6240  xpfi  6590  finomni  6740  indpi  6845  enq0tr  6937  prarloclem3step  6999  distrlem4prl  7087  distrlem4pru  7088  lelttr  7517  nn1suc  8376  nnsub  8395  nn0lt2  8761  uzin  8983  xrlelttr  9203  fzfig  9765  iseqid  9843  iseqz  9846  expival  9856  faclbnd  10046  facavg  10051  ibcval5  10068  hashfzo  10127  iiserex  10621  fisumcvg  10658  fsumf1o  10670  fisumss  10672  fsumcl2lem  10677  absdvdsb  10696  dvdsabsb  10697  dvdsabseq  10730  m1exp1  10783  flodddiv4  10816  gcdaddm  10857  gcdabs1  10862  lcmdvds  10943  prmind2  10984  rpexp  11014
  Copyright terms: Public domain W3C validator