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

Theorem mpjaod 692
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 691 . 2  |-  ( ph  ->  ( ( ps  \/  th )  ->  ch )
)
51, 4mpd 13 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 682
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 683
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  ifbothdc  3474  opth1  4128  onsucelsucexmidlem  4414  reldmtpos  6118  dftpos4  6128  nnm00  6393  xpfi  6786  omp1eomlem  6947  ctmlemr  6961  ctssdclemn0  6963  finomni  6980  indpi  7118  enq0tr  7210  prarloclem3step  7272  distrlem4prl  7360  distrlem4pru  7361  lelttr  7820  nn1suc  8707  nnsub  8727  nn0lt2  9100  uzin  9326  xrlelttr  9557  xlesubadd  9634  fzfig  10171  seq3id  10249  seq3z  10252  faclbnd  10455  facavg  10460  bcval5  10477  hashfzo  10536  iserex  11076  fsum3cvg  11114  fsumf1o  11127  fisumss  11129  fsumcl2lem  11135  fsumadd  11143  fsummulc2  11185  isumsplit  11228  absdvdsb  11438  dvdsabsb  11439  dvdsabseq  11472  m1exp1  11525  flodddiv4  11558  gcdaddm  11599  gcdabs1  11604  lcmdvds  11687  prmind2  11728  rpexp  11758  trilpolemcl  13157  trilpolemlt1  13161
  Copyright terms: Public domain W3C validator