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

Theorem mpjaod 708
 Description: Eliminate a disjunction in a deduction. (Contributed by Mario Carneiro, 29-May-2016.)
Hypotheses
Ref Expression
jaod.1
jaod.2
jaod.3
Assertion
Ref Expression
mpjaod

Proof of Theorem mpjaod
StepHypRef Expression
1 jaod.3 . 2
2 jaod.1 . . 3
3 jaod.2 . . 3
42, 3jaod 707 . 2
51, 4mpd 13 1
 Colors of variables: wff set class Syntax hints:   wi 4   wo 698 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 699 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  ifbothdc  3509  opth1  4166  onsucelsucexmidlem  4452  reldmtpos  6158  dftpos4  6168  nnm00  6433  xpfi  6826  omp1eomlem  6987  ctmlemr  7001  ctssdclemn0  7003  finomni  7020  indpi  7175  enq0tr  7267  prarloclem3step  7329  distrlem4prl  7417  distrlem4pru  7418  lelttr  7877  nn1suc  8764  nnsub  8784  nn0lt2  9157  uzin  9383  xrlelttr  9620  xlesubadd  9697  fzfig  10235  seq3id  10313  seq3z  10316  faclbnd  10520  facavg  10525  bcval5  10542  hashfzo  10601  iserex  11141  fsum3cvg  11180  fsumf1o  11192  fisumss  11194  fsumcl2lem  11200  fsumadd  11208  fsummulc2  11250  isumsplit  11293  absdvdsb  11548  dvdsabsb  11549  dvdsabseq  11582  m1exp1  11635  flodddiv4  11668  gcdaddm  11709  gcdabs1  11714  lcmdvds  11797  prmind2  11838  rpexp  11868  trilpolemcl  13406  trilpolemlt1  13410
 Copyright terms: Public domain W3C validator