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  8703  nnsub  8723  nn0lt2  9090  uzin  9314  xrlelttr  9544  xlesubadd  9621  fzfig  10158  seq3id  10236  seq3z  10239  faclbnd  10442  facavg  10447  bcval5  10464  hashfzo  10523  iserex  11063  fsum3cvg  11101  fsumf1o  11114  fisumss  11116  fsumcl2lem  11122  fsumadd  11130  fsummulc2  11172  isumsplit  11215  absdvdsb  11423  dvdsabsb  11424  dvdsabseq  11457  m1exp1  11510  flodddiv4  11543  gcdaddm  11584  gcdabs1  11589  lcmdvds  11672  prmind2  11713  rpexp  11743  trilpolemcl  13126  trilpolemlt1  13130
  Copyright terms: Public domain W3C validator