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

Theorem mpjaod 690
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 689 . 2  |-  ( ph  ->  ( ( ps  \/  th )  ->  ch )
)
51, 4mpd 13 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 680
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  ifbothdc  3468  opth1  4116  onsucelsucexmidlem  4402  reldmtpos  6102  dftpos4  6112  nnm00  6377  xpfi  6769  omp1eomlem  6929  ctmlemr  6943  ctssdclemn0  6945  finomni  6960  indpi  7092  enq0tr  7184  prarloclem3step  7246  distrlem4prl  7334  distrlem4pru  7335  lelttr  7769  nn1suc  8643  nnsub  8663  nn0lt2  9030  uzin  9254  xrlelttr  9476  xlesubadd  9553  fzfig  10090  seq3id  10168  seq3z  10171  faclbnd  10374  facavg  10379  bcval5  10396  hashfzo  10455  iserex  10994  fsum3cvg  11032  fsumf1o  11045  fisumss  11047  fsumcl2lem  11053  fsumadd  11061  fsummulc2  11103  isumsplit  11146  absdvdsb  11353  dvdsabsb  11354  dvdsabseq  11387  m1exp1  11440  flodddiv4  11473  gcdaddm  11514  gcdabs1  11519  lcmdvds  11600  prmind2  11641  rpexp  11671  trilpolemcl  12911  trilpolemlt1  12915
  Copyright terms: Public domain W3C validator